Context Navigation

source: vis_dev/glu-2.1/src/calPort/calPort.c @ 6

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

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

Download in other formats: