Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

calPort.c @ 26

Last change on this file since 26 was 13, checked in by cecile, 13 years ago
library glu 2.3
File size: 74.3 KB

Line
1	/CFile*********************************************************************
2
3	FileName [calPort.c]
4
5	PackageName [cal_port]
6
7	Synopsis [required]
8
9	Description [optional]
10
11	SeeAlso [optional]
12
13	Author [Rajeev K. Ranjan]
14
15	Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California.
16	All rights reserved.
17
18	Permission is hereby granted, without written agreement and without license
19	or royalty fees, to use, copy, modify, and distribute this software and its
20	documentation for any purpose, provided that the above copyright notice and
21	the following two paragraphs appear in all copies of this software.
22
23	IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
24	DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
25	OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
26	CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
27
28	THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
29	INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
30	FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN
31	"AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
32	MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
33
34	******************************************************************************/
35	#include "calPortInt.h"
36	#ifndef EPD_MAX_BIN
37	#include "epd.h"
38	#endif
39
40	/---------------------------------------------------------------------------/
41	/* Constant declarations */
42	/---------------------------------------------------------------------------/
43
44
45	/---------------------------------------------------------------------------/
46	/* Type declarations */
47	/---------------------------------------------------------------------------/
48
49
50	/---------------------------------------------------------------------------/
51	/* Structure declarations */
52	/---------------------------------------------------------------------------/
53
54
55	/---------------------------------------------------------------------------/
56	/* Variable declarations */
57	/---------------------------------------------------------------------------/
58
59
60	/---------------------------------------------------------------------------/
61	/* Macro declarations */
62	/---------------------------------------------------------------------------/
63
64
65	/AutomaticStart***********************************************************/
66
67	/---------------------------------------------------------------------------/
68	/* Static function prototypes */
69	/---------------------------------------------------------------------------/
70
71	static void InvalidType(FILE file, char field, char *expected);
72
73	/AutomaticEnd*************************************************************/
74
75
76	/---------------------------------------------------------------------------/
77	/* Definition of exported functions */
78	/---------------------------------------------------------------------------/
79
80	/Function******************************************************************
81
82	Synopsis [Function to construct a bdd_t.]
83
84	Description [optional]
85
86	SideEffects [required]
87
88	SeeAlso [optional]
89
90	******************************************************************************/
91	bdd_t *
92	bdd_construct_bdd_t(bdd_manager mgr, bdd_node fn)
93	{
94	bdd_t *result;
95	if (!fn){
96	fail("bdd_construct_bdd_t: possible memory overflow");
97	}
98	result = Cal_MemAlloc(bdd_t, 1);
99	result->bddManager = (Cal_BddManager_t *) mgr;
100	result->calBdd = (Cal_Bdd) fn;
101	result->free = 0;
102	return result;
103	}
104	/Function******************************************************************
105
106	Synopsis [required]
107
108	Description [optional]
109
110	SideEffects [required]
111
112	SeeAlso [optional]
113	******************************************************************************/
114	bdd_package_type_t
115	bdd_get_package_name(void)
116	{
117	return CAL;
118	}
119
120
121	/Function******************************************************************
122
123	Synopsis [required]
124
125	Description [optional]
126
127	SideEffects [required]
128
129	SeeAlso [optional]
130	******************************************************************************/
131	void
132	bdd_end(void *manager)
133	{
134	Cal_BddManager mgr = (Cal_BddManager) manager;
135	void *hooks;
136	hooks = Cal_BddManagerGetHooks(mgr);
137	Cal_MemFree(hooks);
138	Cal_BddManagerQuit(mgr);
139	}
140
141	/Function******************************************************************
142
143	Synopsis [required]
144
145	Description [optional]
146
147	SideEffects [required]
148
149	SeeAlso [optional]
150	******************************************************************************/
151	bdd_manager *
152	bdd_start(int nvariables)
153	{
154	Cal_BddManager mgr;
155	int i;
156	bdd_external_hooks *hooks;
157
158	mgr = Cal_BddManagerInit();
159	for (i = 0; i < nvariables; i++) {
160	(void) Cal_BddManagerCreateNewVarLast(mgr);
161	}
162	hooks = Cal_MemAlloc(bdd_external_hooks, 1);
163	hooks->mdd = hooks->network = hooks->undef1 = (char *) 0;
164	Cal_BddManagerSetHooks(mgr, (void *)hooks);
165	return (bdd_manager *)mgr;
166	}
167
168
169	/Function******************************************************************
170
171	Synopsis [required]
172
173	Description [optional]
174
175	SideEffects [required]
176
177	SeeAlso [optional]
178	******************************************************************************/
179	bdd_t *
180	bdd_create_variable(bdd_manager *manager)
181	{
182	Cal_BddManager mgr = (Cal_BddManager) manager;
183	return bdd_construct_bdd_t(mgr, Cal_BddManagerCreateNewVarLast(mgr));
184	}
185
186	/Function******************************************************************
187
188	Synopsis [required]
189
190	Description [optional]
191
192	SideEffects [required]
193
194	SeeAlso [optional]
195	******************************************************************************/
196	bdd_t *
197	bdd_create_variable_after(bdd_manager *manager, bdd_variableId afterId)
198	{
199	Cal_Bdd afterVar;
200	bdd_t *result;
201	Cal_BddManager mgr = (Cal_BddManager) manager;
202	afterVar = Cal_BddManagerGetVarWithId(mgr, afterId + 1);
203	result = bdd_construct_bdd_t(mgr,
204	Cal_BddManagerCreateNewVarAfter(mgr,
205	afterVar));
206
207	/* No need to free after_var, since single variable BDDs are never garbage collected */
208
209	return result;
210	}
211
212
213
214	/Function******************************************************************
215
216	Synopsis [required]
217
218	Description [optional]
219
220	SideEffects [required]
221
222	SeeAlso [optional]
223	******************************************************************************/
224	bdd_t *
225	bdd_get_variable(bdd_manager *manager, bdd_variableId varId)
226	{
227	Cal_Bdd varBdd;
228	Cal_BddManager mgr = (Cal_BddManager) manager;
229	unsigned int numVars = Cal_BddVars(mgr);
230	if (varId + 1 < numVars) {
231	varBdd = Cal_BddManagerGetVarWithId(mgr, varId + 1);
232	} else {
233	int i;
234	for (i=numVars, varBdd = NULL; i <= varId + 1; i++) {
235	varBdd = Cal_BddManagerCreateNewVarLast(mgr);
236	}
237	}
238	return bdd_construct_bdd_t(mgr, varBdd);
239	}
240
241	/Function******************************************************************
242
243	Synopsis [required]
244
245	Description [optional]
246
247	SideEffects [required]
248
249	SeeAlso [optional]
250	******************************************************************************/
251	bdd_t *
252	bdd_dup(bdd_t *f)
253	{
254	return bdd_construct_bdd_t(f->bddManager, Cal_BddIdentity(f->bddManager, f->calBdd));
255	}
256
257	/Function******************************************************************
258
259	Synopsis [required]
260
261	Description [optional]
262
263	SideEffects [required]
264
265	SeeAlso [optional]
266	******************************************************************************/
267	void
268	bdd_free(bdd_t *f)
269	{
270	if (f == NIL(bdd_t)) {
271	fail("bdd_free: trying to free a NIL bdd_t");
272	}
273	if (f->free){
274	fail("bdd_free: Trying to free a freed bdd_t");
275	}
276	Cal_BddFree(f->bddManager, f->calBdd);
277	f->calBdd = (Cal_Bdd) 0;
278	f->bddManager = NIL(Cal_BddManager_t);
279	f->free = 1;
280	Cal_MemFree(f);
281	}
282
283	/Function******************************************************************
284
285	Synopsis [required]
286
287	Description [optional]
288
289	SideEffects [required]
290
291	SeeAlso [optional]
292	******************************************************************************/
293	bdd_node *
294	bdd_get_node(bdd_t f, boolean isComplemented)
295	{
296	*isComplemented = CAL_TAG0(f->calBdd);
297	return (f->calBdd);
298	}
299
300	/Function******************************************************************
301
302	Synopsis [required]
303
304	Description [optional]
305
306	SideEffects [required]
307
308	SeeAlso [optional]
309	******************************************************************************/
310	bdd_t *
311	bdd_and(bdd_t f,bdd_t g, boolean f_phase, boolean g_phase)
312	{
313	Cal_Bdd temp1, temp2;
314	bdd_t *result;
315	Cal_BddManager mgr;
316
317	mgr = f->bddManager;
318	temp1 = ((f_phase == TRUE) ? Cal_BddIdentity(mgr, f->calBdd) :
319	Cal_BddNot(mgr, f->calBdd));
320	temp2 = ((g_phase == TRUE) ? Cal_BddIdentity(mgr, g->calBdd) :
321	Cal_BddNot(mgr, g->calBdd));
322	result = bdd_construct_bdd_t(mgr, Cal_BddAnd(mgr, temp1, temp2));
323	Cal_BddFree(mgr, temp1);
324	Cal_BddFree(mgr, temp2);
325	return result;
326	}
327
328	/Function******************************************************************
329
330	Synopsis [AND of BDDs with limit on nodes created]
331
332	Description [AND of BDDs with limit on nodes created. This function
333	is not supported by the CAL package. We fall back to the standard AND.]
334
335	SideEffects [required]
336
337	SeeAlso [bdd_and]
338	******************************************************************************/
339	bdd_t *
340	bdd_and_with_limit(bdd_t f, bdd_t g, boolean f_phase, boolean g_phase, unsigned int limit)
341	{
342	return bdd_and(f, g, f_phase, g_phase);
343	}
344
345	bdd_t *
346	bdd_and_array(bdd_t f, array_t g_array, boolean f_phase, boolean g_phase)
347	{
348	Cal_Bdd temp1, temp2, result;
349	bdd_t *g;
350	Cal_BddManager mgr;
351	int i;
352
353	mgr = f->bddManager;
354	result = ((f_phase == TRUE) ? Cal_BddIdentity(mgr, f->calBdd) :
355	Cal_BddNot(mgr, f->calBdd));
356
357	for (i = 0; i < array_n(g_array); i++) {
358	g = array_fetch(bdd_t *, g_array, i);
359	temp1 = result;
360	temp2 = ((g_phase == TRUE) ? Cal_BddIdentity(mgr, g->calBdd) :
361	Cal_BddNot(mgr, g->calBdd));
362	result = Cal_BddAnd(mgr, temp1, temp2);
363	Cal_BddFree(mgr, temp1);
364	Cal_BddFree(mgr, temp2);
365	if (result == NULL)
366	return(NULL);
367	}
368
369	return(bdd_construct_bdd_t(mgr, result));
370	}
371
372	/Function******************************************************************
373
374	Synopsis [required]
375
376	Description [optional]
377
378	SideEffects [required]
379
380	SeeAlso [optional]
381	******************************************************************************/
382	bdd_t *
383	bdd_multiway_and(bdd_manager manager, array_t bddArray)
384	{
385	int i;
386	Cal_Bdd *calBddArray;
387	bdd_t operand, result;
388	Cal_BddManager mgr = (Cal_BddManager) manager;
389
390	calBddArray = Cal_MemAlloc(Cal_Bdd, array_n(bddArray)+1);
391	for (i=0; i<array_n(bddArray); i++){
392	operand = array_fetch(bdd_t*, bddArray, i);
393	calBddArray[i] = operand->calBdd;
394	}
395	calBddArray[i] = (Cal_Bdd)0;
396	result = bdd_construct_bdd_t(mgr,
397	Cal_BddMultiwayAnd(mgr, calBddArray));
398	Cal_MemFree(calBddArray);
399	return result;
400	}
401
402	/Function******************************************************************
403
404	Synopsis [required]
405
406	Description [optional]
407
408	SideEffects [required]
409
410	SeeAlso [optional]
411	******************************************************************************/
412	bdd_t *
413	bdd_multiway_or(bdd_manager manager, array_t bddArray)
414	{
415	int i;
416	Cal_Bdd *calBddArray;
417	bdd_t operand, result;
418	Cal_BddManager mgr = (Cal_BddManager) manager;
419
420	calBddArray = Cal_MemAlloc(Cal_Bdd, array_n(bddArray)+1);
421	for (i=0; i<array_n(bddArray); i++){
422	operand = array_fetch(bdd_t*, bddArray, i);
423	calBddArray[i] = operand->calBdd;
424	}
425	calBddArray[i] = (Cal_Bdd)0;
426	result = bdd_construct_bdd_t(mgr,
427	Cal_BddMultiwayOr(mgr, calBddArray));
428	Cal_MemFree(calBddArray);
429	return result;
430	}
431
432	/Function******************************************************************
433
434	Synopsis [required]
435
436	Description [optional]
437
438	SideEffects [required]
439
440	SeeAlso [optional]
441	******************************************************************************/
442	bdd_t *
443	bdd_multiway_xor(bdd_manager manager, array_t bddArray)
444	{
445	int i;
446	Cal_Bdd *calBddArray;
447	bdd_t operand, result;
448	Cal_BddManager mgr = (Cal_BddManager) manager;
449
450	calBddArray = Cal_MemAlloc(Cal_Bdd, array_n(bddArray)+1);
451	for (i=0; i<array_n(bddArray); i++){
452	operand = array_fetch(bdd_t*, bddArray, i);
453	calBddArray[i] = operand->calBdd;
454	}
455	calBddArray[i] = (Cal_Bdd)0;
456	result = bdd_construct_bdd_t(mgr,
457	Cal_BddMultiwayXor(mgr, calBddArray));
458	Cal_MemFree(calBddArray);
459	return result;
460	}
461
462	/Function******************************************************************
463
464	Synopsis [required]
465
466	Description [optional]
467
468	SideEffects [required]
469
470	SeeAlso [optional]
471	******************************************************************************/
472	array_t *
473	bdd_pairwise_and(bdd_manager manager, array_t bddArray1,
474	array_t *bddArray2)
475	{
476	int i;
477	array_t *resultArray;
478	Cal_Bdd calBddArray, calBddResultArray;
479	bdd_t *operand;
480	Cal_BddManager mgr = (Cal_BddManager) manager;
481
482	if (array_n(bddArray1) != array_n(bddArray2)){
483	fprintf(stderr, "bdd_pairwise_and: Arrays of different lengths.\n");
484	return NIL(array_t);
485	}
486	calBddArray = Cal_MemAlloc(Cal_Bdd, 2*array_n(bddArray1)+1);
487	for (i=0; i<array_n(bddArray1); i++){
488	operand = array_fetch(bdd_t*, bddArray1, i);
489	calBddArray[i<<1] = operand->calBdd;
490	operand = array_fetch(bdd_t*, bddArray2, i);
491	calBddArray[(i<<1)+1] = operand->calBdd;
492	}
493	calBddArray[i<<1] = (Cal_Bdd)0;
494	calBddResultArray = Cal_BddPairwiseAnd(mgr, calBddArray);
495	resultArray = array_alloc(bdd_t*, 0);
496	for (i=0; i<array_n(bddArray1); i++){
497	array_insert_last(bdd_t *, resultArray,
498	bdd_construct_bdd_t(mgr, calBddResultArray[i]));
499	}
500	Cal_MemFree(calBddArray);
501	Cal_MemFree(calBddResultArray);
502	return resultArray;
503	}
504
505	/Function******************************************************************
506
507	Synopsis [required]
508
509	Description [optional]
510
511	SideEffects [required]
512
513	SeeAlso [optional]
514	******************************************************************************/
515	array_t *
516	bdd_pairwise_or(bdd_manager manager, array_t bddArray1,
517	array_t *bddArray2)
518	{
519	int i;
520	array_t *resultArray;
521	Cal_Bdd calBddArray, calBddResultArray;
522	bdd_t *operand;
523	Cal_BddManager mgr = (Cal_BddManager) manager;
524
525	if (array_n(bddArray1) != array_n(bddArray2)){
526	fprintf(stderr, "bdd_pairwise_or: Arrays of different lengths.\n");
527	return NIL(array_t);
528	}
529	calBddArray = Cal_MemAlloc(Cal_Bdd, 2*array_n(bddArray1)+1);
530	for (i=0; i<array_n(bddArray1); i++){
531	operand = array_fetch(bdd_t*, bddArray1, i);
532	calBddArray[i<<1] = operand->calBdd;
533	operand = array_fetch(bdd_t*, bddArray2, i);
534	calBddArray[(i<<1)+1] = operand->calBdd;
535	}
536	calBddArray[i<<1] = (Cal_Bdd)0;
537	calBddResultArray = Cal_BddPairwiseOr(mgr, calBddArray);
538	resultArray = array_alloc(bdd_t*, 0);
539	for (i=0; i<array_n(bddArray1); i++){
540	array_insert_last(bdd_t *, resultArray,
541	bdd_construct_bdd_t(mgr, calBddResultArray[i]));
542	}
543	Cal_MemFree(calBddArray);
544	Cal_MemFree(calBddResultArray);
545	return resultArray;
546	}
547
548
549	/Function******************************************************************
550
551	Synopsis [required]
552
553	Description [optional]
554
555	SideEffects [required]
556
557	SeeAlso [optional]
558	******************************************************************************/
559	array_t *
560	bdd_pairwise_xor(bdd_manager manager, array_t bddArray1,
561	array_t *bddArray2)
562	{
563	int i;
564	array_t *resultArray;
565	Cal_Bdd calBddArray, calBddResultArray;
566	bdd_t *operand;
567	Cal_BddManager mgr = (Cal_BddManager) manager;
568
569	if (array_n(bddArray1) != array_n(bddArray2)){
570	fprintf(stderr, "bdd_pairwise_xor: Arrays of different lengths.\n");
571	return NIL(array_t);
572	}
573	calBddArray = Cal_MemAlloc(Cal_Bdd, 2*array_n(bddArray1)+1);
574	for (i=0; i<array_n(bddArray1); i++){
575	operand = array_fetch(bdd_t*, bddArray1, i);
576	calBddArray[i<<1] = operand->calBdd;
577	operand = array_fetch(bdd_t*, bddArray2, i);
578	calBddArray[(i<<1)+1] = operand->calBdd;
579	}
580	calBddArray[i<<1] = (Cal_Bdd)0;
581	calBddResultArray = Cal_BddPairwiseXor(mgr, calBddArray);
582	resultArray = array_alloc(bdd_t*, 0);
583	for (i=0; i<array_n(bddArray1); i++){
584	array_insert_last(bdd_t *, resultArray,
585	bdd_construct_bdd_t(mgr, calBddResultArray[i]));
586	}
587	Cal_MemFree(calBddArray);
588	Cal_MemFree(calBddResultArray);
589	return resultArray;
590	}
591
592	/Function******************************************************************
593
594	Synopsis [required]
595
596	Description [optional]
597
598	SideEffects [required]
599
600	SeeAlso [optional]
601	******************************************************************************/
602	bdd_t *
603	bdd_and_smooth(bdd_t f, bdd_t g, array_t *smoothingVars)
604	{
605	int num_vars, i;
606	bdd_t fn, result;
607	Cal_Bdd *assoc;
608	Cal_BddManager mgr;
609	int assocId;
610
611	num_vars = array_n(smoothingVars);
612	if (num_vars == 0) {
613	fprintf(stderr,"bdd_and_smooth: no smoothing variables");
614	return bdd_and(f, g, 1, 1);
615	}
616	mgr = f->bddManager;
617	assoc = Cal_MemAlloc(Cal_Bdd, num_vars+1);
618	for (i = 0; i < num_vars; i++) {
619	fn = array_fetch(bdd_t *, smoothingVars, i);
620	assoc[i] = fn->calBdd;
621	}
622	assoc[num_vars] = 0;
623	assocId = Cal_AssociationInit(mgr, assoc, 0);
624	Cal_AssociationSetCurrent(mgr, assocId);
625	result = bdd_construct_bdd_t(mgr, Cal_BddRelProd(mgr, f->calBdd, g->calBdd));
626	Cal_MemFree(assoc);
627	return result;
628	}
629
630	/Function******************************************************************
631
632	Synopsis [required]
633
634	Description [Unsupported: Fall back to standard and_smooth]
635
636	SideEffects [required]
637
638	SeeAlso [bdd_and_smooth]
639
640	******************************************************************************/
641	bdd_t *
642	bdd_and_smooth_with_limit(bdd_t f, bdd_t g, array_t *smoothingVars, unsigned int limit)
643	{
644	return bdd_and_smooth(f, g, smoothingVars);
645	}
646
647	/Function******************************************************************
648
649	Synopsis [required]
650
651	Description [optional]
652
653	SideEffects [required]
654
655	SeeAlso [optional]
656	******************************************************************************/
657	bdd_t *
658	bdd_between(bdd_t fMin, bdd_t fMax)
659	{
660	return bdd_construct_bdd_t(fMin->bddManager,
661	Cal_BddBetween(fMin->bddManager,
662	fMin->calBdd,
663	fMax->calBdd));
664	}
665	/Function******************************************************************
666
667	Synopsis [required]
668
669	Description [optional]
670
671	SideEffects [required]
672
673	SeeAlso [optional]
674	******************************************************************************/
675	bdd_t *
676	bdd_cofactor(bdd_t f,bdd_t g)
677	{
678	return bdd_construct_bdd_t(f->bddManager,
679	Cal_BddCofactor(f->bddManager,
680	f->calBdd,
681	g->calBdd));
682	}
683
684	bdd_t *
685	bdd_cofactor_array(bdd_t f, array_t bddArray)
686	{
687	bdd_t *operand;
688	Cal_Bdd result, temp;
689	int i;
690
691	result = Cal_BddIdentity(f->bddManager, f->calBdd);
692
693	for (i = 0; i < array_n(bddArray); i++) {
694	operand = array_fetch(bdd_t *, bddArray, i);
695	temp = Cal_BddCofactor(f->bddManager, result, operand->calBdd);
696	if (temp == NULL) {
697	Cal_BddFree(f->bddManager, result);
698	return(NULL);
699	}
700	Cal_BddFree(f->bddManager, result);
701	result = temp;
702	}
703
704	return(bdd_construct_bdd_t(f->bddManager, result));
705	}
706
707	/Function******************************************************************
708
709	Synopsis [required]
710
711	Description [optional]
712
713	SideEffects [required]
714
715	SeeAlso [optional]
716	******************************************************************************/
717	bdd_t *
718	bdd_compose(bdd_t f,bdd_t v,bdd_t *g)
719	{
720	return bdd_construct_bdd_t(f->bddManager,
721	Cal_BddCompose(f->bddManager,
722	f->calBdd,
723	v->calBdd,
724	g->calBdd));
725	}
726
727	/Function******************************************************************
728
729	Synopsis [required]
730
731	Description [optional]
732
733	SideEffects [required]
734
735	SeeAlso [optional]
736	******************************************************************************/
737	bdd_t *
738	bdd_consensus(bdd_t f, array_t quantifyingVars)
739	{
740	int num_vars, i;
741	bdd_t fn, result;
742	Cal_Bdd *assoc;
743	Cal_BddManager mgr;
744
745	num_vars = array_n(quantifyingVars);
746	if (num_vars == 0) {
747	fprintf(stderr, "bdd_consensus: no smoothing variables");
748	return f;
749	}
750	mgr = f->bddManager;
751	assoc = Cal_MemAlloc(Cal_Bdd, num_vars+1);
752	for (i = 0; i < num_vars; i++) {
753	fn = array_fetch(bdd_t *, quantifyingVars, i);
754	assoc[i] = fn->calBdd;
755	}
756	assoc[num_vars] = 0;
757	Cal_TempAssociationInit(mgr, assoc, 0);
758	Cal_AssociationSetCurrent(mgr, -1);
759	result = bdd_construct_bdd_t(mgr, Cal_BddForAll(mgr, f->calBdd));
760	Cal_MemFree(assoc);
761	Cal_TempAssociationQuit(mgr);
762	return result;
763	}
764
765	/Function******************************************************************
766
767	Synopsis [required]
768
769	Description [optional]
770
771	SideEffects [required]
772
773	SeeAlso [optional]
774	******************************************************************************/
775	bdd_t *
776	bdd_cproject(bdd_t f,array_t quantifyingVars)
777	{
778	return NIL(bdd_t);
779
780	/*
781	int num_vars, i;
782	bdd_t fn, result;
783	Cal_Bdd_t*assoc;
784	Cal_BddManager mgr;
785
786	if (f == NIL(bdd_t))
787	fail ("bdd_cproject: invalid BDD");
788
789	num_vars = array_n(quantifying_vars);
790	if (num_vars <= 0) {
791	printf("Warning: bdd_cproject: no projection variables\n");
792	result = bdd_dup(f);
793	}
794	else {
795	assoc = Cal_MemAlloc(Cal_Bdd_t, num_vars+1);
796	for (i = 0; i < num_vars; i++) {
797	fn = array_fetch(bdd_t *, quantifying_vars, i);
798	assoc[i] = fn->calBdd;
799	}
800	assoc[num_vars] = (struct bdd_ *) 0;
801	mgr = f->bddManager;
802	cmu_bdd_temp_assoc(mgr, assoc, 0);
803	(void) cmu_bdd_assoc(mgr, -1);
804	result = bdd_construct_bdd_t(mgr, cmu_bdd_project(mgr, f->calBdd));
805	Cal_MemFree(assoc);
806	}
807	return result;
808	*/
809	}
810
811	/Function******************************************************************
812
813	Synopsis [required]
814
815	Description [optional]
816
817	SideEffects [required]
818
819	SeeAlso [optional]
820	******************************************************************************/
821	bdd_t *
822	bdd_else(bdd_t *f)
823	{
824	return bdd_construct_bdd_t(f->bddManager, Cal_BddElse(f->bddManager, f->calBdd));
825	}
826
827	/Function******************************************************************
828
829	Synopsis [required]
830
831	Description [optional]
832
833	SideEffects [required]
834
835	SeeAlso [optional]
836	******************************************************************************/
837	bdd_t *
838	bdd_ite(bdd_t i,bdd_t t,bdd_t *e,boolean i_phase,
839	boolean t_phase,boolean e_phase)
840	{
841	Cal_Bdd temp1, temp2, temp3;
842	bdd_t *result;
843	Cal_BddManager mgr;
844
845	mgr = i->bddManager;
846	temp1 = (i_phase ? Cal_BddIdentity(mgr, i->calBdd) : Cal_BddNot(mgr, i->calBdd));
847	temp2 = (t_phase ? Cal_BddIdentity(mgr, t->calBdd) : Cal_BddNot(mgr, t->calBdd));
848	temp3 = (e_phase ? Cal_BddIdentity(mgr, e->calBdd) : Cal_BddNot(mgr, e->calBdd));
849	result = bdd_construct_bdd_t(mgr, Cal_BddITE(mgr, temp1, temp2, temp3));
850	Cal_BddFree(mgr, temp1);
851	Cal_BddFree(mgr, temp2);
852	Cal_BddFree(mgr, temp3);
853	return result;
854	}
855
856	/Function******************************************************************
857
858	Synopsis [required]
859
860	Description [optional]
861
862	SideEffects [required]
863
864	SeeAlso [optional]
865	******************************************************************************/
866	bdd_t *
867	bdd_minimize(bdd_t f, bdd_t c)
868	{
869	return bdd_construct_bdd_t(f->bddManager,
870	Cal_BddReduce(f->bddManager,
871	f->calBdd, c->calBdd));
872	}
873
874	bdd_t *
875	bdd_minimize_array(bdd_t f, array_t bddArray)
876	{
877	bdd_t *operand;
878	Cal_Bdd result, temp;
879	int i;
880
881	result = Cal_BddIdentity(f->bddManager, f->calBdd);
882	for (i = 0; i < array_n(bddArray); i++) {
883	operand = array_fetch(bdd_t *, bddArray, i);
884	temp = Cal_BddReduce(f->bddManager, result, operand->calBdd);
885	if (temp == NULL) {
886	Cal_BddFree(f->bddManager, result);
887	return(NULL);
888	}
889	Cal_BddFree(f->bddManager, result);
890	result = temp;
891	}
892
893	return(bdd_construct_bdd_t(f->bddManager, result));
894	}
895
896	/Function******************************************************************
897
898	Synopsis [required]
899
900	Description [optional]
901
902	SideEffects [required]
903
904	SeeAlso [optional]
905	******************************************************************************/
906	bdd_t *
907	bdd_not(bdd_t *f)
908	{
909	return bdd_construct_bdd_t(f->bddManager, Cal_BddNot(f->bddManager, f->calBdd));
910	}
911
912	/Function******************************************************************
913
914	Synopsis [required]
915
916	Description [optional]
917
918	SideEffects [required]
919
920	SeeAlso [optional]
921	******************************************************************************/
922	bdd_t *
923	bdd_one(bdd_manager *manager)
924	{
925	Cal_BddManager mgr = (Cal_BddManager) manager;
926	return bdd_construct_bdd_t(mgr, Cal_BddOne(mgr));
927	}
928
929	/Function******************************************************************
930
931	Synopsis [required]
932
933	Description [optional]
934
935	SideEffects [required]
936
937	SeeAlso [optional]
938	******************************************************************************/
939	bdd_t *
940	bdd_or(bdd_t f, bdd_t g, boolean f_phase, boolean g_phase)
941	{
942	Cal_Bdd temp1, temp2;
943	bdd_t *result;
944	Cal_BddManager mgr;
945
946	mgr = f->bddManager;
947	temp1 = (f_phase ? Cal_BddIdentity(mgr, f->calBdd) : Cal_BddNot(mgr, f->calBdd));
948	temp2 = (g_phase ? Cal_BddIdentity(mgr, g->calBdd) : Cal_BddNot(mgr, g->calBdd));
949	result = bdd_construct_bdd_t(mgr, Cal_BddOr(mgr, temp1, temp2));
950	Cal_BddFree(mgr, temp1);
951	Cal_BddFree(mgr, temp2);
952	return result;
953	}
954
955	/Function******************************************************************
956
957	Synopsis [required]
958
959	Description [optional]
960
961	SideEffects [required]
962
963	SeeAlso [optional]
964	******************************************************************************/
965	bdd_t *
966	bdd_smooth(bdd_t f, array_t smoothingVars)
967	{
968	int numVars, i;
969	bdd_t fn, result;
970	Cal_Bdd *assoc;
971	Cal_BddManager mgr;
972	int assocId;
973
974	numVars = array_n(smoothingVars);
975	if (numVars == 0) {
976	fprintf(stderr,"bdd_smooth: no smoothing variables");
977	return f;
978	}
979	mgr = f->bddManager;
980	assoc = Cal_MemAlloc(Cal_Bdd, numVars+1);
981	for (i = 0; i < numVars; i++) {
982	fn = array_fetch(bdd_t *, smoothingVars, i);
983	assoc[i] = fn->calBdd;
984	}
985	assoc[numVars] = 0;
986	assocId = Cal_AssociationInit(mgr, assoc, 0);
987	(void) Cal_AssociationSetCurrent(mgr, assocId); /* set the temp
988	association as the
989	current association
990	*/
991	result = bdd_construct_bdd_t(mgr, Cal_BddExists(mgr, f->calBdd));
992	Cal_MemFree(assoc);
993	return result;
994	}
995
996	/Function******************************************************************
997
998	Synopsis [required]
999
1000	Description [optional]
1001
1002	SideEffects [required]
1003
1004	SeeAlso [optional]
1005	******************************************************************************/
1006	bdd_t *
1007	bdd_substitute(bdd_t f, array_t old_array, array_t *new_array)
1008	{
1009	int num_old_vars, num_new_vars, i;
1010	bdd_t fn_old, fn_new, *result;
1011	Cal_Bdd *assoc;
1012	Cal_BddManager mgr;
1013	int assocId;
1014
1015	num_old_vars = array_n(old_array);
1016	num_new_vars = array_n(new_array);
1017	if (num_old_vars != num_new_vars) {
1018	fprintf(stderr,"bdd_substitute: mismatch of number of new and old variables");
1019	exit(-1);
1020	}
1021	mgr = f->bddManager;
1022	assoc = Cal_MemAlloc(Cal_Bdd, 2*num_old_vars+1);
1023	for (i = 0; i < num_old_vars; i++) {
1024	fn_old = array_fetch(bdd_t *, old_array, i);
1025	fn_new = array_fetch(bdd_t *, new_array, i);
1026	assoc[2*i] = fn_old->calBdd;
1027	assoc[2*i+1] = fn_new->calBdd;
1028	}
1029	assoc[2*num_old_vars] = 0;
1030	assocId = Cal_AssociationInit(mgr, assoc, 1);
1031	(void) Cal_AssociationSetCurrent(mgr, assocId);
1032	result = bdd_construct_bdd_t(mgr, Cal_BddSubstitute(mgr, f->calBdd));
1033	Cal_MemFree(assoc);
1034	Cal_TempAssociationQuit(mgr);
1035	return result;
1036	}
1037
1038	array_t *
1039	bdd_substitute_array(array_t f_array, array_t old_array, array_t *new_array)
1040	{
1041	int i;
1042	bdd_t f, new_;
1043	array_t substitute_array = array_alloc(bdd_t , 0);
1044
1045	arrayForEachItem(bdd_t *, f_array, i, f) {
1046	new_ = bdd_substitute(f, old_array, new_array);
1047	array_insert_last(bdd_t *, substitute_array, new_);
1048	}
1049	return(substitute_array);
1050	}
1051
1052	/Function******************************************************************
1053
1054	Synopsis [Returns the pointer of the BDD.]
1055
1056	Description [optional]
1057
1058	SideEffects [required]
1059
1060	SeeAlso [optional]
1061
1062	******************************************************************************/
1063	void *
1064	bdd_pointer(bdd_t *f)
1065	{
1066	return((void *)f->calBdd);
1067	}
1068
1069	/Function******************************************************************
1070
1071	Synopsis [required]
1072
1073	Description [optional]
1074
1075	SideEffects [required]
1076
1077	SeeAlso [optional]
1078	******************************************************************************/
1079	bdd_t *
1080	bdd_then(bdd_t *f)
1081	{
1082	return bdd_construct_bdd_t(f->bddManager, Cal_BddThen(f->bddManager, f->calBdd));
1083	}
1084
1085	/Function******************************************************************
1086
1087	Synopsis [required]
1088
1089	Description [optional]
1090
1091	SideEffects [required]
1092
1093	SeeAlso [optional]
1094	******************************************************************************/
1095	bdd_t *
1096	bdd_top_var(bdd_t *f)
1097	{
1098	return bdd_construct_bdd_t(f->bddManager, Cal_BddIf(f->bddManager, f->calBdd));
1099	}
1100
1101	/Function******************************************************************
1102
1103	Synopsis [required]
1104
1105	Description [optional]
1106
1107	SideEffects [required]
1108
1109	SeeAlso [optional]
1110	******************************************************************************/
1111	bdd_t *
1112	bdd_xnor(bdd_t f,bdd_t g)
1113	{
1114	return bdd_construct_bdd_t(f->bddManager, Cal_BddXnor(f->bddManager, f->calBdd, g->calBdd));
1115	}
1116
1117	/Function******************************************************************
1118
1119	Synopsis [required]
1120
1121	Description [optional]
1122
1123	SideEffects [required]
1124
1125	SeeAlso [optional]
1126	******************************************************************************/
1127	bdd_t *
1128	bdd_xor(bdd_t f,bdd_t g)
1129	{
1130	return bdd_construct_bdd_t(f->bddManager, Cal_BddXor(f->bddManager, f->calBdd, g->calBdd));
1131	}
1132
1133	/Function******************************************************************
1134
1135	Synopsis [required]
1136
1137	Description [optional]
1138
1139	SideEffects [required]
1140
1141	SeeAlso [optional]
1142	******************************************************************************/
1143	bdd_t *
1144	bdd_zero(bdd_manager *manager)
1145	{
1146	Cal_BddManager mgr = (Cal_BddManager) manager;
1147	return bdd_construct_bdd_t(mgr, Cal_BddZero(mgr));
1148	}
1149
1150	/*
1151	Queries about BDD Formulas ----------------------------------------------------
1152	*/
1153
1154	/Function******************************************************************
1155
1156	Synopsis [required]
1157
1158	Description [optional]
1159
1160	SideEffects [required]
1161
1162	SeeAlso [optional]
1163	******************************************************************************/
1164	boolean
1165	bdd_equal(bdd_t f,bdd_t g)
1166	{
1167	return Cal_BddIsEqual(f->bddManager, f->calBdd, g->calBdd);
1168	}
1169
1170	/Function******************************************************************
1171
1172	Synopsis [required]
1173
1174	Description [optional]
1175
1176	SideEffects [required]
1177
1178	SeeAlso [optional]
1179	******************************************************************************/
1180	boolean
1181	bdd_equal_mod_care_set(bdd_t f, bdd_t g, bdd_t *CareSet)
1182	{
1183	bdd_t *diffBdd;
1184	boolean result;
1185
1186	if (bdd_equal(f, g))
1187	return 1;
1188
1189	diffBdd = bdd_xor(f, g);
1190
1191	result = bdd_leq(diffBdd, CareSet, 1, 0);
1192	bdd_free(diffBdd);
1193
1194	return(result);
1195	}
1196
1197	/Function******************************************************************
1198
1199	Synopsis [required]
1200
1201	Description [optional]
1202
1203	SideEffects [required]
1204
1205	SeeAlso [optional]
1206	******************************************************************************/
1207	bdd_t *
1208	bdd_intersects(bdd_t f,bdd_t g)
1209	{
1210	return bdd_construct_bdd_t(f->bddManager, Cal_BddIntersects(f->bddManager,
1211	f->calBdd,
1212	g->calBdd));
1213	}
1214
1215	/Function******************************************************************
1216
1217	Synopsis [required]
1218
1219	Description [optional]
1220
1221	SideEffects [required]
1222
1223	SeeAlso [optional]
1224	******************************************************************************/
1225	bdd_t *
1226	bdd_closest_cube(bdd_t f,bdd_t g,int *dist)
1227	{
1228	return NIL(bdd_t);
1229	}
1230
1231	/Function******************************************************************
1232
1233	Synopsis [required]
1234
1235	Description [optional]
1236
1237	SideEffects [required]
1238
1239	SeeAlso [optional]
1240	******************************************************************************/
1241	boolean
1242	bdd_is_tautology(bdd_t *f, boolean phase)
1243	{
1244	return ((phase == TRUE) ? Cal_BddIsBddOne(f->bddManager, f->calBdd):
1245	Cal_BddIsBddZero(f->bddManager, f->calBdd));
1246
1247	}
1248
1249	/Function******************************************************************
1250
1251	Synopsis [required]
1252
1253	Description [optional]
1254
1255	SideEffects [required]
1256
1257	SeeAlso [optional]
1258	******************************************************************************/
1259	boolean
1260	bdd_leq(bdd_t f, bdd_t g, boolean f_phase, boolean g_phase)
1261	{
1262	Cal_Bdd temp1, temp2, impliesFn;
1263	Cal_BddManager mgr;
1264	boolean resultValue;
1265
1266	mgr = f->bddManager;
1267	temp1 = (f_phase ? Cal_BddIdentity(mgr, f->calBdd) : Cal_BddNot(mgr, f->calBdd));
1268	temp2 = (g_phase ? Cal_BddIdentity(mgr, g->calBdd) : Cal_BddNot(mgr, g->calBdd));
1269	impliesFn = Cal_BddImplies(mgr, temp1, temp2); /* returns a minterm
1270	of temp1*!temp2
1271	*/
1272	resultValue = Cal_BddIsBddZero(mgr, impliesFn);
1273	Cal_BddFree(mgr, temp1);
1274	Cal_BddFree(mgr, temp2);
1275	Cal_BddFree(mgr, impliesFn);
1276	return resultValue;
1277	}
1278
1279	/Function******************************************************************
1280
1281	Synopsis [required]
1282
1283	Description [optional]
1284
1285	SideEffects [required]
1286
1287	SeeAlso [optional]
1288	******************************************************************************/
1289	boolean
1290	bdd_lequal_mod_care_set(
1291	bdd_t *f,
1292	bdd_t *g,
1293	boolean f_phase,
1294	boolean g_phase,
1295	bdd_t *careSet)
1296	{
1297	bdd_t *temp;
1298	boolean result;
1299
1300	if (bdd_leq(f, g, f_phase, g_phase))
1301	return 1;
1302
1303	temp = bdd_and(f, careSet, f_phase, 1);
1304
1305	result = bdd_leq(temp, g, 1, g_phase);
1306	bdd_free(temp);
1307
1308	return(result);
1309	}
1310
1311	/Function******************************************************************
1312
1313	Synopsis [required]
1314
1315	Description [optional]
1316
1317	SideEffects [required]
1318
1319	SeeAlso [optional]
1320	******************************************************************************/
1321	boolean
1322	bdd_leq_array(bdd_t f, array_t g_array, boolean f_phase, boolean g_phase)
1323	{
1324	int i;
1325	bdd_t *g;
1326	boolean result;
1327
1328	arrayForEachItem(bdd_t *, g_array, i, g) {
1329	result = bdd_leq(f, g, f_phase, g_phase);
1330	if (g_phase) {
1331	if (!result)
1332	return(0);
1333	} else {
1334	if (result)
1335	return(1);
1336	}
1337	}
1338	if (g_phase)
1339	return(1);
1340	else
1341	return(0);
1342	}
1343
1344	/Function******************************************************************
1345
1346	Synopsis [required]
1347
1348	Description [optional]
1349
1350	SideEffects [required]
1351
1352	SeeAlso [optional]
1353	******************************************************************************/
1354	double
1355	bdd_count_onset(bdd_t f, array_t var_array)
1356	{
1357	int numVars;
1358	double fraction;
1359	numVars = array_n(var_array);
1360	fraction = Cal_BddSatisfyingFraction(f->bddManager, f->calBdd);
1361	return (fraction * pow((double) 2, (double) numVars));
1362	}
1363	/Function******************************************************************
1364
1365	Synopsis [Counts the number of minterms in the on set.]
1366
1367	SideEffects []
1368
1369	******************************************************************************/
1370	int
1371	bdd_epd_count_onset(
1372	bdd_t *f,
1373	array_t var_array / of bdd_t 's /,
1374	EpDouble *epd)
1375	{
1376	double nMinterms;
1377
1378	nMinterms = bdd_count_onset(f, var_array);
1379	EpdConvert(nMinterms, epd);
1380	return 0;
1381	} /* end of bdd_epd_count_onset */
1382
1383	/Function******************************************************************
1384
1385	Synopsis [required]
1386
1387	Description [optional]
1388
1389	SideEffects [required]
1390
1391	SeeAlso [optional]
1392	******************************************************************************/
1393	int
1394	bdd_get_free(bdd_t *f)
1395	{
1396	return (f->free);
1397	}
1398
1399	/Function******************************************************************
1400
1401	Synopsis [required]
1402
1403	Description [optional]
1404
1405	SideEffects [required]
1406
1407	SeeAlso [optional]
1408	******************************************************************************/
1409	bdd_manager *
1410	bdd_get_manager(bdd_t *f)
1411	{
1412	return (bdd_manager *) (f->bddManager);
1413	}
1414
1415
1416	/Function******************************************************************
1417
1418	Synopsis [required]
1419
1420	Description [optional]
1421
1422	SideEffects [required]
1423
1424	SeeAlso [optional]
1425	******************************************************************************/
1426	var_set_t *
1427	bdd_get_support(bdd_t *f)
1428	{
1429	Cal_Bdd *support, var;
1430	Cal_BddManager mgr;
1431	long num_vars;
1432	var_set_t *result;
1433	int id, i;
1434
1435	mgr = f->bddManager;
1436	num_vars = Cal_BddVars(mgr);
1437	result = var_set_new((int) num_vars);
1438	support = Cal_MemAlloc(Cal_Bdd, (num_vars+1) * sizeof(Cal_Bdd));
1439	for (i = 0; i <= num_vars; ++i) {
1440	support[i] = 0;
1441	}
1442
1443	(void) Cal_BddSupport(mgr, f->calBdd, support);
1444	for (i = 0; i < num_vars; ++i) {
1445	var = support[i];
1446	if (var) {
1447	id = (int) (Cal_BddGetIfId(mgr, var) - 1);
1448	var_set_set_elt(result, id);
1449	}
1450	}
1451
1452	Cal_MemFree(support);
1453	return result;
1454	}
1455
1456
1457	/Function******************************************************************
1458
1459	Synopsis [Checks whether a BDD is a support of f.]
1460
1461	SideEffects []
1462
1463	******************************************************************************/
1464	int
1465	bdd_is_support_var(bdd_t f, bdd_t var)
1466	{
1467	return(bdd_is_support_var_id(f, bdd_top_var_id(var)));
1468	}
1469
1470
1471	/Function******************************************************************
1472
1473	Synopsis [Checks whether a BDD index is a support of f.]
1474
1475	SideEffects []
1476
1477	******************************************************************************/
1478	int
1479	bdd_is_support_var_id(bdd_t *f, int index)
1480	{
1481	Cal_Bdd *support, var;
1482	Cal_BddManager mgr;
1483	long num_vars;
1484	int id, i;
1485
1486	mgr = f->bddManager;
1487	num_vars = Cal_BddVars(mgr);
1488	support = Cal_MemAlloc(Cal_Bdd, (num_vars+1) * sizeof(Cal_Bdd));
1489	for (i = 0; i <= num_vars; ++i) {
1490	support[i] = 0;
1491	}
1492
1493	(void) Cal_BddSupport(mgr, f->calBdd, support);
1494	for (i = 0; i < num_vars; ++i) {
1495	var = support[i];
1496	if (var) {
1497	id = (int) (Cal_BddGetIfId(mgr, var) - 1);
1498	if (id == index) {
1499	Cal_MemFree(support);
1500	return 1;
1501	}
1502	}
1503	}
1504
1505	Cal_MemFree(support);
1506	return 0;
1507	}
1508
1509
1510	/Function******************************************************************
1511
1512	Synopsis [required]
1513
1514	Description [optional]
1515
1516	SideEffects [required]
1517
1518	SeeAlso [optional]
1519	******************************************************************************/
1520	array_t *
1521	bdd_get_varids(array_t *var_array)
1522	{
1523	int i;
1524	bdd_t *var;
1525	array_t *result;
1526	bdd_variableId varId;
1527
1528	result = array_alloc(bdd_variableId, 0);
1529	for (i = 0; i < array_n(var_array); i++) {
1530	var = array_fetch(bdd_t *, var_array, i);
1531	varId = (int) bdd_top_var_id(var);
1532	array_insert_last(bdd_variableId, result, varId);
1533	}
1534	return result;
1535	}
1536
1537	/Function******************************************************************
1538
1539	Synopsis [required]
1540
1541	Description [optional]
1542
1543	SideEffects [required]
1544
1545	SeeAlso [optional]
1546	******************************************************************************/
1547	unsigned int
1548	bdd_num_vars(bdd_manager *manager)
1549	{
1550	Cal_BddManager mgr = (Cal_BddManager) manager;
1551	return (Cal_BddVars(mgr));
1552	}
1553
1554	/Function******************************************************************
1555
1556	Synopsis [required]
1557
1558	Description [optional]
1559
1560	SideEffects [required]
1561
1562	SeeAlso [optional]
1563	******************************************************************************/
1564	void
1565	bdd_print(bdd_t *f)
1566	{
1567	Cal_BddPrintBdd(f->bddManager, f->calBdd, Cal_BddNamingFnNone,
1568	Cal_BddTerminalIdFnNone, (Cal_Pointer_t) 0, (FILE *)stdout);
1569	}
1570
1571	/Function******************************************************************
1572
1573	Synopsis [required]
1574
1575	Description [optional]
1576
1577	SideEffects [required]
1578
1579	SeeAlso [optional]
1580	******************************************************************************/
1581	void
1582	bdd_print_stats(bdd_manager manager, FILE file)
1583	{
1584	Cal_BddManager mgr = (Cal_BddManager) manager;
1585	Cal_BddManagerGC(mgr);
1586	Cal_BddStats(mgr, file);
1587	}
1588
1589	/Function******************************************************************
1590
1591	Synopsis [required]
1592
1593	Description [optional]
1594
1595	SideEffects [required]
1596
1597	SeeAlso [optional]
1598	******************************************************************************/
1599	int
1600	bdd_size(bdd_t *f)
1601	{
1602	return ((int) Cal_BddSize(f->bddManager, f->calBdd, 1));
1603	}
1604
1605
1606	/Function******************************************************************
1607
1608	Synopsis [Computes the number of nodes of a BDD.]
1609
1610	SideEffects []
1611
1612	******************************************************************************/
1613	int
1614	bdd_node_size(bdd_node *f)
1615	{
1616	return(0);
1617
1618	} /* end of bdd_node_size */
1619
1620	/Function******************************************************************
1621
1622	Synopsis [required]
1623
1624	Description [optional]
1625
1626	SideEffects [required]
1627
1628	SeeAlso [optional]
1629	******************************************************************************/
1630	long
1631	bdd_size_multiple(array_t *bdd_array)
1632	{
1633	long result;
1634	Cal_Bdd *vector_bdd;
1635	bdd_t *f;
1636	int i;
1637	Cal_BddManager mgr;
1638
1639	if ((bdd_array == NIL(array_t)) \|\| (array_n(bdd_array) == 0))
1640	return 0;
1641
1642	f = array_fetch(bdd_t*, bdd_array, 0);
1643	mgr = f->bddManager;
1644	vector_bdd = Cal_MemAlloc(Cal_Bdd, array_n(bdd_array)+1);
1645	for(i=0; i<array_n(bdd_array);i++){
1646	f = array_fetch(bdd_t*, bdd_array, i);
1647	vector_bdd[i] = f->calBdd;
1648	}
1649	vector_bdd[array_n(bdd_array)] = 0;
1650	result = Cal_BddSizeMultiple(mgr, vector_bdd,1);
1651	Cal_MemFree(vector_bdd);
1652	return result;
1653	}
1654
1655	/Function******************************************************************
1656
1657	Synopsis [required]
1658
1659	Description [optional]
1660
1661	SideEffects [required]
1662
1663	SeeAlso [optional]
1664	******************************************************************************/
1665	bdd_variableId
1666	bdd_top_var_id(bdd_t *f)
1667	{
1668	return ((bdd_variableId) (Cal_BddGetIfId(f->bddManager, f->calBdd) - 1));
1669	}
1670
1671	/Function******************************************************************
1672
1673	Synopsis [required]
1674
1675	Description [optional]
1676
1677	SideEffects [required]
1678
1679	SeeAlso [optional]
1680	******************************************************************************/
1681	bdd_external_hooks *
1682	bdd_get_external_hooks(bdd_manager *manager)
1683	{
1684	Cal_BddManager mgr = (Cal_BddManager) manager;
1685	return (bdd_external_hooks *) Cal_BddManagerGetHooks(mgr);
1686	}
1687
1688	/Function******************************************************************
1689
1690	Synopsis [required]
1691
1692	Description [optional]
1693
1694	SideEffects [required]
1695
1696	SeeAlso [optional]
1697	******************************************************************************/
1698	void
1699	bdd_set_gc_mode(bdd_manager *manager,boolean no_gc)
1700	{
1701	Cal_BddManager mgr = (Cal_BddManager) manager;
1702	Cal_BddSetGCMode(mgr, (int) no_gc);
1703	}
1704
1705	/Function******************************************************************
1706
1707	Synopsis [required]
1708
1709	Description [optional]
1710
1711	SideEffects [required]
1712
1713	SeeAlso [optional]
1714	******************************************************************************/
1715	void
1716	bdd_dynamic_reordering(bdd_manager *manager, bdd_reorder_type_t
1717	algorithm_type, bdd_reorder_verbosity_t verbosity)
1718	{
1719	Cal_BddManager mgr = (Cal_BddManager) manager;
1720	switch(algorithm_type) {
1721	case BDD_REORDER_SIFT:
1722	Cal_BddDynamicReordering(mgr, CAL_REORDER_SIFT);
1723	break;
1724	case BDD_REORDER_WINDOW:
1725	Cal_BddDynamicReordering(mgr, CAL_REORDER_WINDOW);
1726	break;
1727	case BDD_REORDER_NONE:
1728	Cal_BddDynamicReordering(mgr, CAL_REORDER_NONE);
1729	break;
1730	default:
1731	fprintf(stderr,"CAL: bdd_dynamic_reordering: unknown algorithm type\n");
1732	fprintf(stderr,"Using SIFT method instead\n");
1733	Cal_BddDynamicReordering(mgr, CAL_REORDER_SIFT);
1734	}
1735
1736	}
1737
1738	void
1739	bdd_dynamic_reordering_zdd(bdd_manager *manager, bdd_reorder_type_t
1740	algorithm_type, bdd_reorder_verbosity_t verbosity)
1741	{
1742	return;
1743	}
1744
1745	/Function******************************************************************
1746
1747	Synopsis [required]
1748
1749	Description [optional]
1750
1751	SideEffects [required]
1752
1753	SeeAlso [optional]
1754	******************************************************************************/
1755	void
1756	bdd_reorder(bdd_manager *manager)
1757	{
1758	Cal_BddManager mgr = (Cal_BddManager) manager;
1759	Cal_BddReorder(mgr);
1760	}
1761
1762	/Function******************************************************************
1763
1764	Synopsis [required]
1765
1766	Description [optional]
1767
1768	SideEffects [required]
1769
1770	SeeAlso [optional]
1771	******************************************************************************/
1772	bdd_variableId
1773	bdd_get_id_from_level(bdd_manager *manager, long level)
1774	{
1775	Cal_Bdd fn;
1776	Cal_BddManager mgr = (Cal_BddManager) manager;
1777	fn = Cal_BddManagerGetVarWithIndex(mgr, level);
1778	if (!fn){
1779	/* variable should always be found, since they are created at bdd_start */
1780	fprintf(stderr, "bdd_get_id_from_level: assumption violated");
1781	exit(-1);
1782	}
1783	return ((bdd_variableId)(Cal_BddGetIfId(mgr, fn) - 1 ));
1784	}
1785
1786	/Function******************************************************************
1787
1788	Synopsis [required]
1789
1790	Description [optional]
1791
1792	SideEffects [required]
1793
1794	SeeAlso [optional]
1795	******************************************************************************/
1796	long
1797	bdd_top_var_level(bdd_manager manager, bdd_t fn)
1798	{
1799	Cal_BddManager mgr = (Cal_BddManager) manager;
1800	return (long)Cal_BddGetIfIndex(mgr, fn->calBdd);
1801	}
1802
1803	/*
1804	*/
1805	/Function******************************************************************
1806
1807	Synopsis [Return TRUE if f is a cube, else return FALSE.]
1808
1809	Description [optional]
1810
1811	SideEffects [required]
1812
1813	SeeAlso [optional]
1814	******************************************************************************/
1815	boolean
1816	bdd_is_cube(bdd_t *f)
1817	{
1818	Cal_BddManager mgr;
1819	if (f == NIL(bdd_t)) {
1820	fail("bdd_is_cube: invalid BDD");
1821	}
1822	if(f->free) fail ("Freed Bdd passed to bdd_is_cube");
1823	mgr = f->bddManager;
1824	return ((boolean)Cal_BddIsCube(mgr, f->calBdd));
1825	}
1826
1827	/Function******************************************************************
1828
1829	Synopsis []
1830
1831	Description [optional]
1832
1833	SideEffects [required]
1834
1835	SeeAlso [optional]
1836	******************************************************************************/
1837	bdd_block *
1838	bdd_new_var_block(bdd_t *f, long length)
1839	{
1840	return (bdd_block *) Cal_BddNewVarBlock(f->bddManager, f->calBdd, length);
1841	}
1842
1843	/Function******************************************************************
1844
1845	Synopsis [Return TRUE if f is a cube, else return FALSE.]
1846
1847	Description [optional]
1848
1849	SideEffects [required]
1850
1851	SeeAlso [optional]
1852	******************************************************************************/
1853	bdd_t *
1854	bdd_var_with_index(bdd_manager *manager, int index)
1855	{
1856	Cal_BddManager mgr = (Cal_BddManager) manager;
1857	return bdd_construct_bdd_t(mgr,
1858	Cal_BddManagerGetVarWithIndex(mgr,
1859	index));
1860	}
1861
1862
1863	/Function******************************************************************
1864
1865	Synopsis [Sets the internal parameters of the package to the given values.]
1866
1867	Description [The CAL package has a set of parameters that can be assigned
1868	different values. This function receives a table which maps strings to
1869	values and sets the parameters represented by the strings to the pertinent
1870	values. Some basic type checking is done. It returns 1 if everything is
1871	correct and 0 otherwise.]
1872
1873	SideEffects []
1874
1875	******************************************************************************/
1876	int
1877	bdd_set_parameters(
1878	bdd_manager *mgr,
1879	avl_tree *valueTable,
1880	FILE *file)
1881	{
1882	/* int reorderMethod; */
1883	st_table *newValueTable;
1884	st_generator *stgen;
1885	avl_generator *avlgen;
1886	char *paramName;
1887	char *paramValue;
1888	Cal_BddManager bddManager = (Cal_BddManager)mgr;
1889
1890
1891	/* Build a new table with the parameter names but with
1892	** the prefix removed. */
1893	newValueTable = st_init_table(st_ptrcmp, st_ptrhash);
1894	avl_foreach_item(valueTable, avlgen, AVL_FORWARD, (char **)&paramName,
1895	(char **)&paramValue) {
1896	if (strncmp(paramName, "BDD.", 4) == 0) {
1897	st_insert(newValueTable, (char *)&paramName[4],
1898	(char *)paramValue);
1899	}
1900	}
1901
1902	st_foreach_item(newValueTable, stgen, &paramName, &paramValue) {
1903	unsigned int uvalue;
1904	double value;
1905	char *invalidChar;
1906
1907	invalidChar = NIL(char);
1908
1909	if (strcmp(paramName, "Node limit") == 0) {
1910	uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10);
1911	/* RB an unsigned will never be < 0 */
1912	if (invalidChar /\|\| uvalue < 0*/) {
1913	InvalidType(file, "Node limit", "unsigned integer");
1914	}
1915	else {
1916	bddManager->nodeLimit = uvalue;
1917	}
1918	}
1919	else if (strcmp(paramName, "Garbage collection enabled") == 0) {
1920	if (strcmp(paramValue, "yes") == 0) {
1921	bddManager->gcMode = 1;
1922	}
1923	else if (strcmp(paramValue, "no") == 0) {
1924	bddManager->gcMode = 0;
1925	}
1926	else {
1927	InvalidType(file, "Garbage collection enabled", "(yes,no)");
1928	}
1929	}
1930	else if (strcmp(paramName,
1931	"Maximum number of variables sifted per reordering") == 0) {
1932	uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10);
1933	if (invalidChar /\|\| uvalue < 0*/) {
1934	InvalidType(file, "Maximum number of variables sifted per reordering",
1935	"unsigned integer");
1936	}
1937	else {
1938	bddManager->maxNumVarsSiftedPerReordering = uvalue;
1939	}
1940	}
1941	else if (strcmp(paramName,
1942	"Maximum number of variable swaps per reordering") == 0) {
1943	uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10);
1944	if (invalidChar /\|\| uvalue < 0*/) {
1945	InvalidType(file, "Maximum number of variable swaps per reordering",
1946	"unsigned integer");
1947	}
1948	else {
1949	bddManager->maxNumSwapsPerReordering = uvalue;
1950	}
1951	}
1952	else if (strcmp(paramName,
1953	"Maximum growth while sifting a variable") == 0) {
1954	value = strtod(paramValue, &invalidChar);
1955	if (*invalidChar) {
1956	InvalidType(file, "Maximum growth while sifting a variable",
1957	"real");
1958	}
1959	else {
1960	bddManager->maxSiftingGrowth = value;
1961	}
1962	}
1963	else if (strcmp(paramName, "Dynamic reordering of BDDs enabled") == 0) {
1964	if (strcmp(paramValue, "yes") == 0) {
1965	bddManager->dynamicReorderingEnableFlag = 1;
1966	}
1967	else if (strcmp(paramValue, "no") == 0) {
1968	bddManager->dynamicReorderingEnableFlag = 0;
1969	}
1970	else {
1971	InvalidType(file, "Dynamic reordering of BDDs enabled",
1972	"(yes,no)");
1973	}
1974	}
1975	else if (strcmp(paramName, "Use old reordering")
1976	== 0) {
1977	if (strcmp(paramValue, "yes") == 0) {
1978	bddManager->reorderMethod = CAL_REORDER_METHOD_BF;
1979	}
1980	else if (strcmp(paramValue, "no") == 0) {
1981	bddManager->reorderMethod = CAL_REORDER_METHOD_DF;
1982	}
1983	else {
1984	InvalidType(file, "Dynamic reordering of BDDs enabled",
1985	"(yes,no)");
1986	}
1987	}
1988	else if (strcmp(paramName, "Dynamic reordering threshold") == 0) {
1989	uvalue = (unsigned int) strtol(paramValue, &invalidChar, 10);
1990	if (invalidChar /\|\| uvalue < 0*/) {
1991	InvalidType(file, "Dynamic reordering threshold", "unsigned integer");
1992	}
1993	else {
1994	bddManager->reorderingThreshold = uvalue;
1995	}
1996	}
1997	else if (strcmp(paramName, "Repacking after GC threshold")
1998	== 0) {
1999	value = strtod(paramValue, &invalidChar);
2000	if (*invalidChar \|\| value < 0) {
2001	InvalidType(file, "Repacking after GC threshold", "unsigned real");
2002	}
2003	else {
2004	bddManager->repackAfterGCThreshold = value;
2005	}
2006	}
2007	else if (strcmp(paramName, "Table repacking threshold")
2008	== 0) {
2009	value = strtod(paramValue, &invalidChar);
2010	if (*invalidChar \|\| value < 0) {
2011	InvalidType(file, "Table repacking threshold", "unsigned real");
2012	}
2013	else {
2014	bddManager->tableRepackThreshold = value;
2015	}
2016	}
2017	else {
2018	(void) fprintf(file, "Warning: Parameter %s not recognized.",
2019	paramName);
2020	(void) fprintf(file, " Ignored.\n");
2021	}
2022	} /* end of st_foreach_item */
2023
2024	/* Clean up. */
2025	st_free_table(newValueTable);
2026
2027	return(1);
2028
2029	} /* end of bdd_set_parameters */
2030
2031	/Function******************************************************************
2032
2033	Synopsis [Dummy functions defined in bdd.h]
2034
2035	SideEffects []
2036
2037	******************************************************************************/
2038	bdd_t *
2039	bdd_compact(bdd_t f, bdd_t g)
2040	{
2041	return 0;
2042	}
2043
2044	bdd_t *
2045	bdd_squeeze(bdd_t f, bdd_t g)
2046	{
2047	return 0;
2048	}
2049	bdd_t *
2050	bdd_clipping_and_smooth(
2051	bdd_t *f,
2052	bdd_t *g,
2053	array_t smoothing_vars / of bdd_t 's /,
2054	int maxDepth,
2055	int over)
2056	{
2057	return NIL(bdd_t);
2058	}
2059
2060	bdd_t *
2061	bdd_approx_hb(
2062	bdd_t *f,
2063	bdd_approx_dir_t approxDir,
2064	int numVars,
2065	int threshold)
2066	{
2067	return NIL(bdd_t);
2068	}
2069
2070	bdd_t *
2071	bdd_approx_sp(
2072	bdd_t *f,
2073	bdd_approx_dir_t approxDir,
2074	int numVars,
2075	int threshold,
2076	int hardlimit)
2077	{
2078	return NIL(bdd_t);
2079	}
2080
2081	bdd_t *
2082	bdd_approx_ua(
2083	bdd_t *f,
2084	bdd_approx_dir_t approxDir,
2085	int numVars,
2086	int threshold,
2087	int safe,
2088	double quality)
2089	{
2090	return NIL(bdd_t);
2091	}
2092
2093	bdd_t *
2094	bdd_approx_remap_ua(
2095	bdd_t *f,
2096	bdd_approx_dir_t approxDir,
2097	int numVars,
2098	int threshold,
2099	double quality)
2100	{
2101	return NIL(bdd_t);
2102	}
2103
2104	bdd_t *
2105	bdd_approx_biased_rua(
2106	bdd_t *f,
2107	bdd_approx_dir_t approxDir,
2108	bdd_t *bias,
2109	int numVars,
2110	int threshold,
2111	double quality,
2112	double quality1)
2113	{
2114	return NIL(bdd_t);
2115	}
2116
2117	bdd_t *
2118	bdd_approx_compress(
2119	bdd_t *f,
2120	bdd_approx_dir_t approxDir,
2121	int numVars,
2122	int threshold)
2123	{
2124	return NIL(bdd_t);
2125	}
2126
2127	int
2128	bdd_gen_decomp(
2129	bdd_t *f,
2130	bdd_partition_type_t partType,
2131	bdd_t ***conjArray)
2132	{
2133	return 0;
2134	}
2135
2136	int
2137	bdd_var_decomp(
2138	bdd_t *f,
2139	bdd_partition_type_t partType,
2140	bdd_t ***conjArray)
2141	{
2142	return 0;
2143	}
2144
2145	int
2146	bdd_approx_decomp(
2147	bdd_t *f,
2148	bdd_partition_type_t partType,
2149	bdd_t ***conjArray)
2150	{
2151	return 0;
2152	}
2153
2154	int
2155	bdd_add_hook(
2156	bdd_manager *mgr,
2157	int (procedure)(bdd_manager , char , void ),
2158	bdd_hook_type_t whichHook)
2159	{
2160	return 0;
2161	}
2162
2163	int
2164	bdd_remove_hook(
2165	bdd_manager *mgr,
2166	int (procedure)(bdd_manager , char , void ),
2167	bdd_hook_type_t whichHook)
2168	{
2169	return 0;
2170	}
2171
2172	int
2173	bdd_enable_reordering_reporting(bdd_manager *mgr)
2174	{
2175	return 0;
2176	}
2177	int
2178	bdd_disable_reordering_reporting(bdd_manager *mgr)
2179	{
2180	return 0;
2181	}
2182
2183	bdd_reorder_verbosity_t
2184	bdd_reordering_reporting(bdd_manager *mgr)
2185	{
2186	return BDD_REORDER_VERBOSITY_DEFAULT;
2187	}
2188
2189	int
2190	bdd_print_apa_minterm(
2191	FILE *fp,
2192	bdd_t *f,
2193	int nvars,
2194	int precision)
2195	{
2196	return 0;
2197	}
2198
2199	int
2200	bdd_apa_compare_ratios(
2201	int nvars,
2202	bdd_t *f1,
2203	bdd_t *f2,
2204	int f1Num,
2205	int f2Num)
2206	{
2207	return 0;
2208	}
2209
2210	int
2211	bdd_iter_decomp(
2212	bdd_t *f,
2213	bdd_partition_type_t partType,
2214	bdd_t ***conjArray)
2215	{
2216	return 0;
2217	}
2218
2219	bdd_t *
2220	bdd_solve_eqn(
2221	bdd_t *f,
2222	array_t *g,
2223	array_t *unknowns)
2224	{
2225	return NIL(bdd_t);
2226	}
2227
2228	int
2229	bdd_reordering_status(
2230	bdd_manager *mgr,
2231	bdd_reorder_type_t *method)
2232	{
2233	return 0;
2234	}
2235
2236	int
2237	bdd_read_node_count(bdd_manager *mgr)
2238	{
2239	return 0;
2240	}
2241
2242	double
2243	bdd_correlation(bdd_t f, bdd_t g)
2244	{
2245	return 0.0;
2246	}
2247
2248
2249	bdd_t *
2250	bdd_pick_one_minterm(bdd_t f, array_t varsArray)
2251	{
2252	return NIL(bdd_t);
2253	}
2254
2255	array_t *
2256	bdd_bdd_pick_arbitrary_minterms(
2257	bdd_t *f,
2258	array_t *varsArray,
2259	int n,
2260	int k)
2261	{
2262	return NIL(array_t);
2263	}
2264
2265
2266	int
2267	bdd_reordering_zdd_status(
2268	bdd_manager *mgr,
2269	bdd_reorder_type_t *method)
2270	{
2271	return 0;
2272	}
2273
2274
2275	bdd_node *
2276	bdd_bdd_to_add(
2277	bdd_manager *mgr,
2278	bdd_node *fn)
2279	{
2280	return NIL(bdd_node);
2281	}
2282
2283	bdd_node *
2284	bdd_add_permute(
2285	bdd_manager *mgr,
2286	bdd_node *fn,
2287	int *permut)
2288	{
2289	return NIL(bdd_node);
2290	}
2291
2292	bdd_node *
2293	bdd_bdd_permute(
2294	bdd_manager *mgr,
2295	bdd_node *fn,
2296	int *permut)
2297	{
2298	return NIL(bdd_node);
2299	}
2300
2301
2302	void
2303	bdd_ref(bdd_node *fn)
2304	{
2305	return ;
2306	}
2307
2308
2309	void
2310	bdd_recursive_deref(bdd_manager mgr, bdd_node f)
2311	{
2312	return;
2313	}
2314
2315
2316	bdd_node *
2317	bdd_add_exist_abstract(
2318	bdd_manager *mgr,
2319	bdd_node *fn,
2320	bdd_node *vars)
2321	{
2322	return NIL(bdd_node);
2323	}
2324
2325
2326	bdd_node *
2327	bdd_add_apply(
2328	bdd_manager *mgr,
2329	bdd_node (operation)(bdd_manager , bdd_node , bdd_node *),
2330	bdd_node *fn1,
2331	bdd_node *fn2)
2332	{
2333	return NIL(bdd_node);
2334	}
2335
2336
2337	bdd_node *
2338	bdd_add_nonsim_compose(
2339	bdd_manager *mgr,
2340	bdd_node *fn,
2341	bdd_node **vector)
2342	{
2343	return NIL(bdd_node);
2344	}
2345
2346
2347	bdd_node *
2348	bdd_add_residue(
2349	bdd_manager *mgr,
2350	int n,
2351	int m,
2352	int options,
2353	int top)
2354	{
2355	return NIL(bdd_node);
2356	}
2357
2358
2359	bdd_node *
2360	bdd_add_vector_compose(
2361	bdd_manager *mgr,
2362	bdd_node *fn,
2363	bdd_node **vector)
2364	{
2365	return NIL(bdd_node);
2366	}
2367
2368
2369	bdd_node *
2370	bdd_add_times(
2371	bdd_manager *mgr,
2372	bdd_node **fn1,
2373	bdd_node **fn2)
2374	{
2375	return NIL(bdd_node);
2376	}
2377
2378
2379	int
2380	bdd_check_zero_ref(bdd_manager *mgr)
2381	{
2382	return 0;
2383	}
2384
2385
2386	void
2387	bdd_dynamic_reordering_disable(bdd_manager *mgr)
2388	{
2389	return;
2390	}
2391
2392	void
2393	bdd_dynamic_reordering_zdd_disable(bdd_manager *mgr)
2394	{
2395	return;
2396	}
2397
2398
2399	bdd_node *
2400	bdd_add_xnor(
2401	bdd_manager *mgr,
2402	bdd_node **fn1,
2403	bdd_node **fn2)
2404	{
2405	return NIL(bdd_node);
2406	}
2407
2408
2409	int
2410	bdd_shuffle_heap(
2411	bdd_manager *mgr,
2412	int *permut)
2413	{
2414	return 0;
2415	}
2416
2417
2418	bdd_node *
2419	bdd_add_compose(
2420	bdd_manager *mgr,
2421	bdd_node *fn1,
2422	bdd_node *fn2,
2423	int var)
2424	{
2425	return NIL(bdd_node);
2426	}
2427
2428
2429	bdd_node *
2430	bdd_add_ith_var(
2431	bdd_manager *mgr,
2432	int i)
2433	{
2434	return NIL(bdd_node);
2435	}
2436
2437
2438	int
2439	bdd_get_level_from_id(
2440	bdd_manager *mgr,
2441	int id)
2442	{
2443	return 0;
2444	}
2445
2446
2447	bdd_node *
2448	bdd_bdd_exist_abstract(
2449	bdd_manager *mgr,
2450	bdd_node *fn,
2451	bdd_node *cube)
2452	{
2453	return NIL(bdd_node);
2454	}
2455
2456
2457	int
2458	bdd_equal_sup_norm(
2459	bdd_manager *mgr,
2460	bdd_node *fn,
2461	bdd_node *gn,
2462	BDD_VALUE_TYPE tolerance,
2463	int pr)
2464	{
2465	return 0;
2466	}
2467
2468
2469	bdd_node *
2470	bdd_read_logic_zero(bdd_manager *mgr)
2471	{
2472	return NIL(bdd_node);
2473	}
2474
2475
2476	bdd_node *
2477	bdd_bdd_ith_var(
2478	bdd_manager *mgr,
2479	int i)
2480	{
2481	return NIL(bdd_node);
2482	}
2483
2484
2485	bdd_node *
2486	bdd_add_divide(
2487	bdd_manager *mgr,
2488	bdd_node **fn1,
2489	bdd_node **fn2)
2490	{
2491	return NIL(bdd_node);
2492	}
2493
2494
2495	bdd_node *
2496	bdd_bdd_constrain(
2497	bdd_manager *mgr,
2498	bdd_node *f,
2499	bdd_node *c)
2500	{
2501	return NIL(bdd_node);
2502	}
2503
2504	bdd_node *
2505	bdd_bdd_restrict(
2506	bdd_manager *mgr,
2507	bdd_node *f,
2508	bdd_node *c)
2509	{
2510	return NIL(bdd_node);
2511	}
2512
2513
2514	bdd_node *
2515	bdd_add_hamming(
2516	bdd_manager *mgr,
2517	bdd_node **xVars,
2518	bdd_node **yVars,
2519	int nVars)
2520	{
2521	return NIL(bdd_node);
2522	}
2523
2524
2525	bdd_node *
2526	bdd_add_ite(
2527	bdd_manager *mgr,
2528	bdd_node *f,
2529	bdd_node *g,
2530	bdd_node *h)
2531	{
2532	return NIL(bdd_node);
2533	}
2534
2535
2536	bdd_node *
2537	bdd_add_find_max(
2538	bdd_manager *mgr,
2539	bdd_node *f)
2540	{
2541	return NIL(bdd_node);
2542	}
2543
2544
2545	int
2546	bdd_bdd_pick_one_cube(
2547	bdd_manager *mgr,
2548	bdd_node *node,
2549	char *string)
2550	{
2551	return 0;
2552	}
2553
2554
2555	bdd_node *
2556	bdd_add_swap_variables(
2557	bdd_manager *mgr,
2558	bdd_node *f,
2559	bdd_node **x,
2560	bdd_node **y,
2561	int n)
2562	{
2563	return NIL(bdd_node);
2564	}
2565
2566	bdd_node *
2567	bdd_bdd_swap_variables(
2568	bdd_manager *mgr,
2569	bdd_node *f,
2570	bdd_node **x,
2571	bdd_node **y,
2572	int n)
2573	{
2574	return NIL(bdd_node);
2575	}
2576
2577
2578	bdd_node *
2579	bdd_bdd_or(
2580	bdd_manager *mgr,
2581	bdd_node *f,
2582	bdd_node *g)
2583	{
2584	return NIL(bdd_node);
2585	}
2586
2587	bdd_t *
2588	bdd_compute_cube(
2589	bdd_manager *mgr,
2590	array_t *vars)
2591	{
2592	return NIL(bdd_t);
2593	}
2594
2595	bdd_t *
2596	bdd_compute_cube_with_phase(
2597	bdd_manager *mgr,
2598	array_t *vars,
2599	array_t *phase)
2600	{
2601	return NIL(bdd_t);
2602	}
2603
2604
2605	bdd_node *
2606	bdd_bdd_compute_cube(
2607	bdd_manager *mgr,
2608	bdd_node **vars,
2609	int *phase,
2610	int n)
2611	{
2612	return NIL(bdd_node);
2613	}
2614
2615
2616	bdd_node *
2617	bdd_indices_to_cube(
2618	bdd_manager *mgr,
2619	int *idArray,
2620	int n)
2621	{
2622	return NIL(bdd_node);
2623	}
2624
2625
2626	bdd_node *
2627	bdd_bdd_and(
2628	bdd_manager *mgr,
2629	bdd_node *f,
2630	bdd_node *g)
2631	{
2632	return NIL(bdd_node);
2633	}
2634
2635
2636	bdd_node *
2637	bdd_add_matrix_multiply(
2638	bdd_manager *mgr,
2639	bdd_node *A,
2640	bdd_node *B,
2641	bdd_node **z,
2642	int nz)
2643	{
2644	return NIL(bdd_node);
2645	}
2646
2647
2648	bdd_node *
2649	bdd_add_compute_cube(
2650	bdd_manager *mgr,
2651	bdd_node **vars,
2652	int *phase,
2653	int n)
2654	{
2655	return NIL(bdd_node);
2656	}
2657
2658
2659	bdd_node *
2660	bdd_add_const(
2661	bdd_manager *mgr,
2662	BDD_VALUE_TYPE c)
2663	{
2664	return NIL(bdd_node);
2665	}
2666
2667
2668	double
2669	bdd_count_minterm(
2670	bdd_manager *mgr,
2671	bdd_node *f,
2672	int n)
2673	{
2674	return 0;
2675	}
2676
2677
2678	bdd_node *
2679	bdd_add_bdd_threshold(
2680	bdd_manager *mgr,
2681	bdd_node *f,
2682	BDD_VALUE_TYPE value)
2683	{
2684	return NIL(bdd_node);
2685	}
2686
2687
2688	bdd_node *
2689	bdd_add_bdd_strict_threshold(
2690	bdd_manager *mgr,
2691	bdd_node *f,
2692	BDD_VALUE_TYPE value)
2693	{
2694	return NIL(bdd_node);
2695	}
2696
2697	BDD_VALUE_TYPE
2698	bdd_read_epsilon(bdd_manager *mgr)
2699	{
2700	return 0;
2701	}
2702
2703	bdd_node *
2704	bdd_read_one(bdd_manager *mgr)
2705	{
2706	return NIL(bdd_node);
2707	}
2708
2709
2710	bdd_node *
2711	bdd_bdd_pick_one_minterm(
2712	bdd_manager *mgr,
2713	bdd_node *f,
2714	bdd_node **vars,
2715	int n)
2716	{
2717	return NIL(bdd_node);
2718	}
2719
2720
2721	bdd_node *
2722	bdd_read_zero(bdd_manager *mgr)
2723	{
2724	return NIL(bdd_node);
2725	}
2726
2727
2728	bdd_node *
2729	bdd_bdd_new_var(bdd_manager *mgr)
2730	{
2731	return NIL(bdd_node);
2732	}
2733
2734
2735	bdd_node *
2736	bdd_bdd_and_abstract(
2737	bdd_manager *mgr,
2738	bdd_node *f,
2739	bdd_node *g,
2740	bdd_node *cube)
2741	{
2742	return NIL(bdd_node);
2743	}
2744
2745	void
2746	bdd_deref(bdd_node *f)
2747	{
2748	return;
2749	}
2750
2751	bdd_node *
2752	bdd_add_plus(
2753	bdd_manager *mgr,
2754	bdd_node **fn1,
2755	bdd_node **fn2)
2756	{
2757	return NIL(bdd_node);
2758	}
2759
2760
2761	int
2762	bdd_read_reorderings(bdd_manager *mgr)
2763	{
2764	return 0;
2765	}
2766
2767	int
2768	bdd_read_next_reordering(bdd_manager *mgr)
2769	{
2770	return 0;
2771	}
2772
2773	void
2774	bdd_set_next_reordering(bdd_manager *mgr, int next)
2775	{
2776	}
2777
2778	bdd_node *
2779	bdd_bdd_xnor(
2780	bdd_manager *mgr,
2781	bdd_node *f,
2782	bdd_node *g)
2783	{
2784	return NIL(bdd_node);
2785	}
2786
2787	bdd_node *
2788	bdd_bdd_vector_compose(
2789	bdd_manager *mgr,
2790	bdd_node *f,
2791	bdd_node **vector)
2792	{
2793	return NIL(bdd_node);
2794	}
2795
2796	bdd_node *
2797	bdd_extract_node_as_is(bdd_t *fn)
2798	{
2799	return NIL(bdd_node);
2800	}
2801
2802
2803	bdd_node *
2804	bdd_zdd_get_node(
2805	bdd_manager *mgr,
2806	int id,
2807	bdd_node *g,
2808	bdd_node *h)
2809	{
2810	return NIL(bdd_node);
2811	}
2812
2813	bdd_node *
2814	bdd_zdd_product(
2815	bdd_manager *mgr,
2816	bdd_node *f,
2817	bdd_node *g)
2818	{
2819	return NIL(bdd_node);
2820	}
2821
2822	bdd_node *
2823	bdd_zdd_product_recur(
2824	bdd_manager *mgr,
2825	bdd_node *f,
2826	bdd_node *g)
2827	{
2828	return NIL(bdd_node);
2829	}
2830
2831	bdd_node *
2832	bdd_zdd_union(
2833	bdd_manager *mgr,
2834	bdd_node *f,
2835	bdd_node *g)
2836	{
2837	return(NIL(bdd_node));
2838	}
2839
2840
2841	bdd_node *
2842	bdd_zdd_weak_div(
2843	bdd_manager *mgr,
2844	bdd_node *f,
2845	bdd_node *g)
2846	{
2847	return NIL(bdd_node);
2848	}
2849
2850	bdd_node *
2851	bdd_zdd_weak_div_recur(
2852	bdd_manager *mgr,
2853	bdd_node *f,
2854	bdd_node *g)
2855	{
2856	return NIL(bdd_node);
2857	}
2858
2859	bdd_node *
2860	bdd_zdd_isop_recur(
2861	bdd_manager *mgr,
2862	bdd_node *L,
2863	bdd_node *U,
2864	bdd_node **zdd_I)
2865	{
2866	return NIL(bdd_node);
2867	}
2868
2869	bdd_node *
2870	bdd_zdd_isop(
2871	bdd_manager *mgr,
2872	bdd_node *L,
2873	bdd_node *U,
2874	bdd_node **zdd_I)
2875	{
2876	return NIL(bdd_node);
2877	}
2878
2879	int
2880	bdd_zdd_get_cofactors3(
2881	bdd_manager *mgr,
2882	bdd_node *f,
2883	int v,
2884	bdd_node **f1,
2885	bdd_node **f0,
2886	bdd_node **fd)
2887	{
2888	return 0;
2889	}
2890
2891	bdd_node *
2892	bdd_bdd_and_recur(
2893	bdd_manager *mgr,
2894	bdd_node *f,
2895	bdd_node *g)
2896	{
2897	return NIL(bdd_node);
2898	}
2899
2900	bdd_node *
2901	bdd_unique_inter(
2902	bdd_manager *mgr,
2903	int v,
2904	bdd_node *f,
2905	bdd_node *g)
2906	{
2907	return NIL(bdd_node);
2908	}
2909
2910	bdd_node *
2911	bdd_unique_inter_ivo(
2912	bdd_manager *mgr,
2913	int v,
2914	bdd_node *f,
2915	bdd_node *g)
2916	{
2917	return NIL(bdd_node);
2918	}
2919
2920
2921	bdd_node *
2922	bdd_zdd_diff(
2923	bdd_manager *mgr,
2924	bdd_node *f,
2925	bdd_node *g)
2926	{
2927	return NIL(bdd_node);
2928	}
2929
2930	bdd_node *
2931	bdd_zdd_diff_recur(
2932	bdd_manager *mgr,
2933	bdd_node *f,
2934	bdd_node *g)
2935	{
2936	return NIL(bdd_node);
2937	}
2938
2939	int
2940	bdd_num_zdd_vars(bdd_manager *mgr)
2941	{
2942	return -1;
2943	}
2944
2945	bdd_node *
2946	bdd_regular(bdd_node *f)
2947	{
2948	return NIL(bdd_node);
2949	}
2950
2951	int
2952	bdd_is_constant(bdd_node *f)
2953	{
2954	return 0;
2955	}
2956
2957	int
2958	bdd_is_complement(bdd_node *f)
2959	{
2960	return 0;
2961	}
2962
2963	bdd_node *
2964	bdd_bdd_T(bdd_node *f)
2965	{
2966	return NIL(bdd_node);
2967	}
2968
2969	bdd_node *
2970	bdd_bdd_E(bdd_node *f)
2971	{
2972	return NIL(bdd_node);
2973	}
2974
2975	bdd_node *
2976	bdd_not_bdd_node(bdd_node *f)
2977	{
2978	return NIL(bdd_node);
2979	}
2980
2981	void
2982	bdd_recursive_deref_zdd(
2983	bdd_manager *mgr,
2984	bdd_node *f)
2985	{
2986	return;
2987	}
2988
2989	int
2990	bdd_zdd_count(
2991	bdd_manager *mgr,
2992	bdd_node *f)
2993	{
2994	return 0;
2995	}
2996
2997	int
2998	bdd_read_zdd_level(
2999	bdd_manager *mgr,
3000	int index)
3001	{
3002	return -1;
3003	}
3004
3005	int
3006	bdd_zdd_vars_from_bdd_vars(
3007	bdd_manager *mgr,
3008	int multiplicity)
3009	{
3010	return 0;
3011	}
3012
3013	void
3014	bdd_zdd_realign_enable(bdd_manager *mgr)
3015	{
3016	return;
3017	}
3018
3019	void
3020	bdd_zdd_realign_disable(bdd_manager *mgr)
3021	{
3022	return;
3023	}
3024
3025	int
3026	bdd_zdd_realignment_enabled(bdd_manager *mgr)
3027	{
3028	return 0;
3029	}
3030
3031	void
3032	bdd_realign_enable(bdd_manager *mgr)
3033	{
3034	return;
3035	}
3036
3037	void
3038	bdd_realign_disable(bdd_manager *mgr)
3039	{
3040	return;
3041	}
3042
3043	int
3044	bdd_realignment_enabled(bdd_manager *mgr)
3045	{
3046	return 0;
3047	}
3048
3049	int
3050	bdd_node_read_index(bdd_node *f)
3051	{
3052	return -1;
3053	}
3054
3055	bdd_node *
3056	bdd_read_next(bdd_node *f)
3057	{
3058	return NIL(bdd_node);
3059	}
3060
3061	void
3062	bdd_set_next(bdd_node f, bdd_node g)
3063	{
3064	return;
3065	}
3066
3067	int
3068	bdd_read_reordered_field(bdd_manager *mgr)
3069	{
3070	return -1;
3071	}
3072
3073	void
3074	bdd_set_reordered_field(bdd_manager *mgr, int n)
3075	{
3076	return;
3077	}
3078
3079	bdd_node *
3080	bdd_add_apply_recur(
3081	bdd_manager *mgr,
3082	bdd_node (operation)(bdd_manager , bdd_node , bdd_node *),
3083	bdd_node *fn1,
3084	bdd_node *fn2)
3085	{
3086	return NIL(bdd_node);
3087	}
3088
3089
3090	BDD_VALUE_TYPE
3091	bdd_add_value(bdd_node *f)
3092	{
3093	return 0.0;
3094	}
3095
3096	int
3097	bdd_print_minterm(bdd_t *f)
3098	{
3099	return 0;
3100	}
3101
3102
3103	int
3104	bdd_print_cover(bdd_t *f)
3105	{
3106	return 0;
3107	}
3108
3109
3110	bdd_t *
3111	bdd_xor_smooth(
3112	bdd_t *f,
3113	bdd_t *g,
3114	array_t *smoothing_vars)
3115	{
3116	return NIL(bdd_t);
3117	}
3118
3119
3120	bdd_node *
3121	bdd_read_plus_infinity(bdd_manager *mgr)
3122	{
3123	return NIL(bdd_node);
3124
3125	} /* end of bdd_read_plus_infinity */
3126
3127
3128
3129	bdd_node *
3130	bdd_priority_select(
3131	bdd_manager *mgr,
3132	bdd_node *R,
3133	bdd_node **x,
3134	bdd_node **y,
3135	bdd_node **z,
3136	bdd_node *Pi,
3137	int n,
3138	bdd_node (Pifunc)(bdd_manager , int, bdd_node , bdd_node , bdd_node *))
3139	{
3140	return NIL(bdd_node);
3141
3142	} /* end of bdd_priority_select */
3143
3144
3145	void
3146	bdd_set_background(
3147	bdd_manager *mgr,
3148	bdd_node *f)
3149	{
3150	return;
3151
3152	} /* end of bdd_set_background */
3153
3154
3155	bdd_node *
3156	bdd_read_background(bdd_manager *mgr)
3157	{
3158	return NIL(bdd_node);
3159
3160	} /* end of bdd_read_background */
3161
3162
3163	bdd_node *
3164	bdd_bdd_cofactor(
3165	bdd_manager *mgr,
3166	bdd_node *f,
3167	bdd_node *g)
3168	{
3169	return NIL(bdd_node);
3170
3171	} /* end of bdd_bdd_cofactor */
3172
3173
3174	bdd_node *
3175	bdd_bdd_ite(
3176	bdd_manager *mgr,
3177	bdd_node *f,
3178	bdd_node *g,
3179	bdd_node *h)
3180	{
3181	return NIL(bdd_node);
3182
3183	} /* end of bdd_bdd_ite */
3184
3185
3186	bdd_node *
3187	bdd_add_minus(
3188	bdd_manager *mgr,
3189	bdd_node **fn1,
3190	bdd_node **fn2)
3191	{
3192	return NIL(bdd_node);
3193
3194	} /* end of bdd_add_plus */
3195
3196
3197	bdd_node *
3198	bdd_dxygtdxz(
3199	bdd_manager *mgr,
3200	int N,
3201	bdd_node **x,
3202	bdd_node **y,
3203	bdd_node **z)
3204	{
3205	return NIL(bdd_node);
3206
3207	} /* end of bdd_dxygtdxz */
3208
3209
3210	bdd_node *
3211	bdd_bdd_univ_abstract(
3212	bdd_manager *mgr,
3213	bdd_node *fn,
3214	bdd_node *vars)
3215	{
3216	return NIL(bdd_node);
3217
3218	} /* end of bdd_bdd_univ_abstract */
3219
3220
3221	bdd_node *
3222	bdd_bdd_cprojection(
3223	bdd_manager *mgr,
3224	bdd_node *R,
3225	bdd_node *Y)
3226	{
3227	return NIL(bdd_node);
3228
3229	} /* end of bdd_bdd_cprojection */
3230
3231	bdd_node *
3232	bdd_xeqy(
3233	bdd_manager *mgr,
3234	int N,
3235	bdd_node **x,
3236	bdd_node **y)
3237	{
3238	return NIL(bdd_node);
3239
3240	} /* end of bdd_xeqy */
3241
3242	bdd_node *
3243	bdd_add_roundoff(
3244	bdd_manager *mgr,
3245	bdd_node *f,
3246	int N)
3247	{
3248	return NIL(bdd_node);
3249
3250	} /* end of bdd_add_roundoff */
3251
3252	bdd_node *
3253	bdd_xgty(
3254	bdd_manager *mgr,
3255	int N,
3256	bdd_node **x,
3257	bdd_node **y)
3258	{
3259	return NIL(bdd_node);
3260
3261	} /* end of bdd_xgty */
3262
3263	bdd_node *
3264	bdd_add_cmpl(
3265	bdd_manager *mgr,
3266	bdd_node *f)
3267	{
3268	return NIL(bdd_node);
3269
3270	} /* end of bdd_add_cmpl */
3271
3272	bdd_node *
3273	bdd_split_set(
3274	bdd_manager *mgr,
3275	bdd_node *f,
3276	bdd_node **x,
3277	int n,
3278	double m)
3279	{
3280	return NIL(bdd_node);
3281
3282	} /* end of bdd_split_set */
3283
3284
3285	int
3286	bdd_debug_check(bdd_manager *mgr)
3287	{
3288	return -1;
3289
3290	} /* end of bdd_debug_check */
3291
3292	bdd_node *
3293	bdd_bdd_xor(
3294	bdd_manager *mgr,
3295	bdd_node *f,
3296	bdd_node *g)
3297	{
3298	return NIL(bdd_node);
3299	}
3300
3301	void
3302	bdd_dump_blif(
3303	bdd_manager *mgr,
3304	int nBdds,
3305	bdd_node **bdds,
3306	char **inames,
3307	char **onames,
3308	char *model,
3309	FILE *fp)
3310	{
3311	return;
3312	}
3313
3314	void
3315	bdd_dump_blif_body(
3316	bdd_manager *mgr,
3317	int nBdds,
3318	bdd_node **bdds,
3319	char **inames,
3320	char **onames,
3321	FILE *fp)
3322	{
3323	return;
3324	}
3325
3326	void
3327	bdd_dump_dot(
3328	bdd_manager *mgr,
3329	int nBdds,
3330	bdd_node **bdds,
3331	char **inames,
3332	char **onames,
3333	FILE *fp)
3334	{
3335	return;
3336	}
3337
3338	bdd_node *
3339	bdd_make_bdd_from_zdd_cover(bdd_manager mgr, bdd_node node)
3340	{
3341	return(NIL(bdd_node));
3342	}
3343
3344	bdd_node *
3345	bdd_zdd_complement(bdd_manager mgr, bdd_node node)
3346	{
3347	return(NIL(bdd_node));
3348	}
3349
3350	bdd_node *
3351	bdd_bdd_vector_support(
3352	bdd_manager *mgr,
3353	bdd_node **F,
3354	int n)
3355	{
3356	return NIL(bdd_node);
3357	}
3358
3359	int
3360	bdd_bdd_vector_support_size(
3361	bdd_manager *mgr,
3362	bdd_node **F,
3363	int n)
3364	{
3365	return -1;
3366	}
3367
3368
3369	int
3370	bdd_bdd_support_size(
3371	bdd_manager *mgr,
3372	bdd_node *F)
3373	{
3374	return -1;
3375	}
3376
3377	bdd_node *
3378	bdd_bdd_support(
3379	bdd_manager *mgr,
3380	bdd_node *F)
3381	{
3382	return NIL(bdd_node);
3383	}
3384
3385	bdd_node *
3386	bdd_add_general_vector_compose(
3387	bdd_manager *mgr,
3388	bdd_node *f,
3389	bdd_node **vectorOn,
3390	bdd_node **vectorOff)
3391	{
3392	return NIL(bdd_node);
3393	}
3394
3395	int
3396	bdd_bdd_leq(
3397	bdd_manager *mgr,
3398	bdd_node *f,
3399	bdd_node *g)
3400	{
3401	return -1;
3402	}
3403
3404	bdd_node *
3405	bdd_bdd_boolean_diff(
3406	bdd_manager *mgr,
3407	bdd_node *f,
3408	int x)
3409	{
3410	return NIL(bdd_node);
3411	}
3412
3413	/Function******************************************************************
3414
3415	Synopsis [Compares two bdds are same.]
3416
3417	SideEffects []
3418
3419	******************************************************************************/
3420	int
3421	bdd_ptrcmp(bdd_t f, bdd_t g)
3422	{
3423	if (f->calBdd == g->calBdd)
3424	return(0);
3425	else
3426	return(1);
3427	}
3428
3429
3430	/Function******************************************************************
3431
3432	Synopsis [Returns the hash value of a bdd.]
3433
3434	SideEffects []
3435
3436	******************************************************************************/
3437	int
3438	bdd_ptrhash(bdd_t *f, int size)
3439	{
3440	int hash;
3441
3442	hash = (int)((unsigned long)f->calBdd >> 2) % size;
3443	return(hash);
3444	}
3445
3446	bdd_t *
3447	bdd_subset_with_mask_vars(
3448	bdd_t *f,
3449	array_t *varsArray,
3450	array_t *maskVarsArray)
3451	{
3452	return NIL(bdd_t);
3453	}
3454
3455	bdd_t *
3456	bdd_and_smooth_with_cube(
3457	bdd_t *f,
3458	bdd_t *g,
3459	bdd_t *cube)
3460	{
3461	return NIL(bdd_t);
3462	}
3463
3464	bdd_t *
3465	bdd_smooth_with_cube(bdd_t f, bdd_t cube)
3466	{
3467	int i;
3468	bdd_t var, res;
3469	array_t *smoothingVars;
3470	var_set_t *supportVarSet;
3471
3472	smoothingVars = array_alloc(bdd_t *, 0);
3473	supportVarSet = bdd_get_support(f);
3474	for (i = 0; i < supportVarSet->n_elts; i++) {
3475	if (var_set_get_elt(supportVarSet, i) == 1) {
3476	var = bdd_var_with_index(f->bddManager, i);
3477	array_insert_last(bdd_t *, smoothingVars, var);
3478	}
3479	}
3480	var_set_free(supportVarSet);
3481
3482	res = bdd_smooth(f, smoothingVars);
3483
3484	for (i = 0; i < array_n(smoothingVars); i++) {
3485	var = array_fetch(bdd_t *, smoothingVars, i);
3486	bdd_free(var);
3487	}
3488	array_free(smoothingVars);
3489	return res;
3490	}
3491
3492	bdd_t *
3493	bdd_substitute_with_permut(bdd_t f, int permut)
3494	{
3495	return NIL(bdd_t);
3496	}
3497
3498	array_t *
3499	bdd_substitute_array_with_permut(array_t f_array, int permut)
3500	{
3501	return NIL(array_t);
3502	}
3503
3504	bdd_t *
3505	bdd_vector_compose(
3506	bdd_t *f,
3507	array_t *varArray,
3508	array_t *funcArray)
3509	{
3510	return NIL(bdd_t);
3511	}
3512
3513	double *
3514	bdd_cof_minterm(bdd_t *f)
3515	{
3516	return(NIL(double));
3517	}
3518
3519	int
3520	bdd_var_is_dependent(
3521	bdd_t *f,
3522	bdd_t *var)
3523	{
3524	return(0);
3525	}
3526
3527	array_t *
3528	bdd_find_essential(bdd_t *f)
3529	{
3530	return(NIL(array_t));
3531	}
3532
3533	bdd_t *
3534	bdd_find_essential_cube(bdd_t *f)
3535	{
3536	return(NIL(bdd_t));
3537	}
3538
3539	int
3540	bdd_estimate_cofactor(
3541	bdd_t *f,
3542	bdd_t *var,
3543	int phase)
3544	{
3545	return(0);
3546	}
3547
3548	long
3549	bdd_read_peak_memory(bdd_manager *mgr)
3550	{
3551	return(0);
3552	}
3553
3554	int
3555	bdd_read_peak_live_node(bdd_manager *mgr)
3556	{
3557	return(0);
3558	}
3559
3560	int
3561	bdd_set_pi_var(
3562	bdd_manager *mgr,
3563	int index)
3564	{
3565	return(0);
3566	}
3567
3568	int
3569	bdd_set_ps_var(
3570	bdd_manager *mgr,
3571	int index)
3572	{
3573	return(0);
3574	}
3575
3576	int
3577	bdd_set_ns_var(
3578	bdd_manager *mgr,
3579	int index)
3580	{
3581	return(0);
3582	}
3583
3584	int
3585	bdd_is_pi_var(
3586	bdd_manager *mgr,
3587	int index)
3588	{
3589	return(0);
3590	}
3591
3592	int
3593	bdd_is_ps_var(
3594	bdd_manager *mgr,
3595	int index)
3596	{
3597	return(0);
3598	}
3599
3600	int
3601	bdd_is_ns_var(
3602	bdd_manager *mgr,
3603	int index)
3604	{
3605	return(0);
3606	}
3607
3608	int
3609	bdd_set_pair_index(
3610	bdd_manager *mgr,
3611	int index,
3612	int pairIndex)
3613	{
3614	return(0);
3615	}
3616
3617	int
3618	bdd_read_pair_index(
3619	bdd_manager *mgr,
3620	int index)
3621	{
3622	return(0);
3623	}
3624
3625	int
3626	bdd_set_var_to_be_grouped(
3627	bdd_manager *mgr,
3628	int index)
3629	{
3630	return(0);
3631	}
3632
3633	int
3634	bdd_set_var_hard_group(
3635	bdd_manager *mgr,
3636	int index)
3637	{
3638	return(0);
3639	}
3640
3641	int
3642	bdd_reset_var_to_be_grouped(
3643	bdd_manager *mgr,
3644	int index)
3645	{
3646	return(0);
3647	}
3648
3649	int
3650	bdd_is_var_to_be_grouped(
3651	bdd_manager *mgr,
3652	int index)
3653	{
3654	return(0);
3655	}
3656
3657	int
3658	bdd_is_var_hard_group(
3659	bdd_manager *mgr,
3660	int index)
3661	{
3662	return(0);
3663	}
3664
3665	int
3666	bdd_is_var_to_be_ungrouped(
3667	bdd_manager *mgr,
3668	int index)
3669	{
3670	return(0);
3671	}
3672
3673	int
3674	bdd_set_var_to_be_ungrouped(
3675	bdd_manager *mgr,
3676	int index)
3677	{
3678	return(0);
3679	}
3680
3681	int
3682	bdd_bind_var(
3683	bdd_manager *mgr,
3684	int index)
3685	{
3686	return(0);
3687	}
3688
3689	int
3690	bdd_unbind_var(
3691	bdd_manager *mgr,
3692	int index)
3693	{
3694	return(0);
3695	}
3696
3697	int
3698	bdd_is_lazy_sift(bdd_manager *mgr)
3699	{
3700	return(0);
3701	}
3702
3703	void
3704	bdd_discard_all_var_groups(bdd_manager *mgr)
3705	{
3706	return;
3707	}
3708
3709	/---------------------------------------------------------------------------/
3710	/* Definition of internal functions */
3711	/---------------------------------------------------------------------------/
3712
3713
3714	/---------------------------------------------------------------------------/
3715	/* Definition of static functions */
3716	/---------------------------------------------------------------------------/
3717
3718	/Function******************************************************************
3719
3720	Synopsis [Function to print a warning that an illegal value was read.]
3721
3722	SideEffects []
3723
3724	SeeAlso [bdd_set_parameters]
3725
3726	******************************************************************************/
3727	static void
3728	InvalidType(
3729	FILE *file,
3730	char *field,
3731	char *expected)
3732	{
3733	(void) fprintf(file, "Warning: In parameter \"%s\"\n", field);
3734	(void) fprintf(file, "Illegal type detected. %s expected\n", expected);
3735
3736	} /* end of InvalidType */

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

Context Navigation

source: vis_dev/glu-2.3/src/calPort/calPort.c @ 26

Download in other formats: