Biddy  2.1.1
A multi-platform Binary Decision Diagrams package
biddyMain.c
Go to the documentation of this file.
1 /***************************************************************************/
45 #include "biddyInt.h"
46 
47 #ifdef UNIX
48 #include <unistd.h> /* used for sysconf(), UNIX only */
49 #include <sys/resource.h> /* used for setrlimit(), UNIX only */
50 #include <sys/time.h> /* used for initialization of random numbers, UNIX only */
51 #endif
52 
53 #ifdef UNIXXX
54 #include <malloc.h> /* experimental */
55 #endif
56 
57 /*----------------------------------------------------------------------------*/
58 /* Constant declarations */
59 /*----------------------------------------------------------------------------*/
60 
61 /* ALL SIZES ARE unsigned int */
62 /* Size of node and cache tables must be 2^N-1 */
63 /* e.g. 2^16-1 = 65535, 2^20-1 = 1048575, 2^24-1 = 16777215 */
64 
65 /* If BDD node is 24B (e.g. 32-bit GNU/Linux systems) */
66 /* 256 nodes is 6 kB */
67 /* 65536 nodes is 1.5 MB */
68 /* 262144 nodes is 6 MB */
69 /* 524288 nodes is 12 MB */
70 /* 1048576 nodes is 24.0 MB */
71 /* 2097152 nodes is 48.0 MB */
72 /* 4194304 nodes is 96.0 MB */
73 /* 8388608 nodes is 192.0 MB */
74 /* 16777216 nodes is 384.0 MB */
75 
76 /* If BDD node is 48B (e.g. 64-bit GNU/Linux systems), then: */
77 /* 256 nodes is 12 kB */
78 /* 65536 nodes is 3.0 MB */
79 /* 262144 nodes is 12 MB */
80 /* 524288 nodes is 24 MB */
81 /* 1048576 nodes is 48.0 MB */
82 /* 2097152 nodes is 96.0 MB */
83 /* 4194304 nodes is 192.0 MB */
84 /* 8388608 nodes is 384.0 MB */
85 /* 16777216 nodes is 768.0 MB */
86 
87 #define TINY_SIZE 1023
88 #define SMALL_SIZE 65535
89 #define MEDIUM_SIZE 262143
90 #define LARGE_SIZE 1048575
91 #define XLARGE_SIZE 2097151
92 #define XXLARGE_SIZE 4194303
93 #define XXXLARGE_SIZE 8388607
94 #define HUGE_SIZE 16777215
95 
96 /*----------------------------------------------------------------------------*/
97 /* Variable declarations */
98 /*----------------------------------------------------------------------------*/
99 
100 /* EXPORTED VARIABLES */
101 
102 #ifdef __cplusplus
103 extern "C" {
104 #endif
105 
106 #ifdef __cplusplus
107 }
108 #endif
109 
110 /* INTERNAL VARIABLES */
111 
112 Biddy_Manager biddyAnonymousManager /* anonymous manager */
113  = NULL;
114 
115 BiddyLocalInfo *biddyLocalInfo /* local info table */
116  = NULL;
117 
118 /* Biddy_Edge debug_edge = NULL; */ /* debugging, only */
119 /* Biddy_Boolean biddySiftingActive = FALSE; */ /* debugging, only */
120 
121 /*----------------------------------------------------------------------------*/
122 /* Static function prototypes */
123 /*----------------------------------------------------------------------------*/
124 
125 static Biddy_Boolean isEqv(Biddy_Manager MNG1, Biddy_Edge f1, Biddy_Manager MNG2, Biddy_Edge f2);
126 static BiddyLocalInfo * createLocalInfo(Biddy_Manager MNG, Biddy_Edge f, BiddyLocalInfo *c);
127 static void deleteLocalInfo(Biddy_Manager MNG, Biddy_Edge f);
128 static inline unsigned int nodeTableHash(Biddy_Variable v, Biddy_Edge pf, Biddy_Edge pt, unsigned int size);
129 static inline void addNodeTable(Biddy_Manager MNG, unsigned int hash, BiddyNode *node, BiddyNode *sup1);
130 static inline BiddyNode *findNodeTable(Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge pf, Biddy_Edge pt, BiddyNode **thesup);
131 static void addVariableElement(Biddy_Manager MNG, Biddy_String x, Biddy_Boolean varelem, Biddy_Boolean complete);
132 static void evalProbability(Biddy_Manager MNG, Biddy_Edge f, double *c1, double *c0, Biddy_Boolean *leftmost);
133 static Biddy_Boolean checkFunctionOrdering(Biddy_Manager MNG, Biddy_Edge f);
134 static Biddy_Variable getGlobalOrdering(Biddy_Manager MNG, Biddy_Variable v);
135 static Biddy_Variable swapWithHigher(Biddy_Manager MNG, Biddy_Variable v, Biddy_Boolean *active);
136 static Biddy_Variable swapWithLower(Biddy_Manager MNG, Biddy_Variable v, Biddy_Boolean *active);
137 static void swapVariables(Biddy_Manager MNG, Biddy_Variable low, Biddy_Variable high, Biddy_Boolean *active);
138 static void oneSwap(Biddy_Manager MNG, BiddyNode *sup, Biddy_Variable low, Biddy_Variable high, Biddy_Edge *u0, Biddy_Edge *u1);
139 static void oneSwapEdge(Biddy_Manager MNG, Biddy_Edge sup, Biddy_Variable low, Biddy_Variable high, Biddy_Edge *u, Biddy_Boolean *active);
140 static void nullOrdering(BiddyOrderingTable table);
141 static void alphabeticOrdering(Biddy_Manager MNG, BiddyOrderingTable table);
142 static void nodeNumberOrdering(Biddy_Manager MNG, Biddy_Edge f, unsigned int *i, BiddyOrderingTable ordering);
143 /* static void reorderVariables(Biddy_Manager MNG, int numV, BiddyVariableOrder *tableV, int numN, BiddyNodeList *tableN, int id); */ /* NOT IMPLEMENTED, YET */
144 static void constructBDD(Biddy_Manager MNG, int numN, BiddyNodeList *tableN, int id);
145 static void concat(char **s1, const char *s2);
146 static void debugNode(Biddy_Manager MNG, BiddyNode *node);
147 static void debugEdge(Biddy_Manager MNG, Biddy_Edge edge);
148 
149 /* debugging */
150 
151 static void writeORDER(Biddy_Manager MNG);
152 static void debugORDERING(Biddy_Manager MNG, BiddyOrderingTable table, Biddy_Variable varnum);
153 
154 
155 /* currently, not used */
156 /*
157 static void writeBDD(Biddy_Manager MNG, Biddy_Edge f);
158 static void warshall(BiddyOrderingTable table, Biddy_Variable varnum);
159 */
160 
161 /*----------------------------------------------------------------------------*/
162 /* Definition of exported functions */
163 /*----------------------------------------------------------------------------*/
164 
165 /***************************************************************************/
183 #ifdef __cplusplus
184 extern "C" {
185 #endif
186 
187 void
188 Biddy_InitMNG(Biddy_Manager *mng, int bddtype)
189 {
190  BiddyInitMNG(mng,bddtype);
191 }
192 
193 #ifdef __cplusplus
194 }
195 #endif
196 
197 /***************************************************************************/
208 #ifdef __cplusplus
209 extern "C" {
210 #endif
211 
212 void
214 {
215  BiddyExitMNG(mng);
216 }
217 
218 #ifdef __cplusplus
219 }
220 #endif
221 
222 /***************************************************************************/
230 #ifdef __cplusplus
231 extern "C" {
232 #endif
233 
236 {
237  return BiddyAbout();
238 }
239 
240 #ifdef __cplusplus
241 }
242 #endif
243 
244 /***************************************************************************/
255 #ifdef __cplusplus
256 extern "C" {
257 #endif
258 
261 {
262  Biddy_Edge r;
263 
264  if (BiddyIsTerminal(fun)) return fun;
265 
266  r = BiddyT(fun);
267 
268  /* EXTERNAL FUNCTIONS MUST RETURN NON-OBSOLETE NODE */
269  if ((BiddyN(r)->expiry) &&
270  ((BiddyN(r)->expiry<BiddyN(fun)->expiry) || !(BiddyN(fun)->expiry))
271  )
272  {
273  BiddyN(r)->expiry = BiddyN(fun)->expiry;
274  }
275 
276  return r;
277 }
278 
279 #ifdef __cplusplus
280 }
281 #endif
282 
283 /***************************************************************************/
294 #ifdef __cplusplus
295 extern "C" {
296 #endif
297 
300 {
301  Biddy_Edge r;
302 
303  if (BiddyIsTerminal(fun)) return fun;
304 
305  r = BiddyE(fun);
306 
307  /* EXTERNAL FUNCTIONS MUST RETURN NON-OBSOLETE NODE */
308  if ((BiddyN(r)->expiry) &&
309  ((BiddyN(r)->expiry<BiddyN(fun)->expiry) || !(BiddyN(fun)->expiry))
310  )
311  {
312  BiddyN(r)->expiry = BiddyN(fun)->expiry;
313  }
314 
315  return r;
316 }
317 
318 #ifdef __cplusplus
319 }
320 #endif
321 
322 /***************************************************************************/
332 #ifdef __cplusplus
333 extern "C" {
334 #endif
335 
338 {
339  return BiddyV(fun);
340 }
341 
342 #ifdef __cplusplus
343 }
344 #endif
345 
346 /***************************************************************************/
358 #ifdef __cplusplus
359 extern "C" {
360 #endif
361 
364 {
365  if (!MNG) MNG = biddyAnonymousManager;
366 
367  if (biddyManagerType == BIDDYTYPEOBDD) {
368  /* IMPLEMENTED */
369  }
370  else if (biddyManagerType == BIDDYTYPEOBDDC) {
371  /* IMPLEMENTED */
372  }
373 #ifndef COMPACT
374  else if (biddyManagerType == BIDDYTYPEZBDD) {
375  /* IMPLEMENTED */
376  }
377  else if (biddyManagerType == BIDDYTYPEZBDDC) {
378  /* IMPLEMENTED */
379  }
380  else if (biddyManagerType == BIDDYTYPETZBDD) {
381  /* IMPLEMENTED */
382  }
383 #endif
384  else {
385  fprintf(stderr,"Biddy_Managed_GetTerminal: Unsupported BDD type!\n");
386  return biddyNull;
387  }
388 
389  return biddyTerminal;
390 }
391 
392 #ifdef __cplusplus
393 }
394 #endif
395 
396 /***************************************************************************/
410 #ifdef __cplusplus
411 extern "C" {
412 #endif
413 
416 {
417  if (!MNG) MNG = biddyAnonymousManager;
418 
419  if (biddyManagerType == BIDDYTYPEOBDD) {
420  /* IMPLEMENTED */
421  }
422  else if (biddyManagerType == BIDDYTYPEOBDDC) {
423  /* IMPLEMENTED */
424  }
425 #ifndef COMPACT
426  else if (biddyManagerType == BIDDYTYPEZBDD) {
427  /* IMPLEMENTED */
428  }
429  else if (biddyManagerType == BIDDYTYPEZBDDC) {
430  /* IMPLEMENTED */
431  }
432  else if (biddyManagerType == BIDDYTYPETZBDD) {
433  /* IMPLEMENTED */
434  }
435 #endif
436  else {
437  fprintf(stderr,"Biddy_Managed_GetConstantZero: Unsupported BDD type!\n");
438  return biddyNull;
439  }
440 
441  return biddyZero;
442 }
443 
444 #ifdef __cplusplus
445 }
446 #endif
447 
448 /***************************************************************************/
464 #ifdef __cplusplus
465 extern "C" {
466 #endif
467 
470 {
471  if (!MNG) MNG = biddyAnonymousManager;
472 
473  if (biddyManagerType == BIDDYTYPEOBDD) {
474  /* IMPLEMENTED */
475  }
476  else if (biddyManagerType == BIDDYTYPEOBDDC) {
477  /* IMPLEMENTED */
478  }
479 #ifndef COMPACT
480  else if (biddyManagerType == BIDDYTYPEZBDD) {
481  /* IMPLEMENTED */
482  }
483  else if (biddyManagerType == BIDDYTYPEZBDDC) {
484  /* IMPLEMENTED */
485  }
486  else if (biddyManagerType == BIDDYTYPETZBDD) {
487  /* IMPLEMENTED */
488  }
489 #endif
490  else {
491  fprintf(stderr,"Biddy_Managed_GetConstantOne: Unsupported BDD type!\n");
492  return biddyNull;
493  }
494 
495  return biddyOne;
496 }
497 
498 #ifdef __cplusplus
499 }
500 #endif
501 
502 /***************************************************************************/
513 #ifdef __cplusplus
514 extern "C" {
515 #endif
516 
519 {
520  if (!MNG) MNG = biddyAnonymousManager;
521 
522  if (biddyManagerType == BIDDYTYPEOBDD) {
523  /* IMPLEMENTED */
524  }
525  else if (biddyManagerType == BIDDYTYPEOBDDC) {
526  /* IMPLEMENTED */
527  }
528 #ifndef COMPACT
529  else if (biddyManagerType == BIDDYTYPEZBDD) {
530  /* IMPLEMENTED */
531  }
532  else if (biddyManagerType == BIDDYTYPEZBDDC) {
533  /* IMPLEMENTED */
534  }
535  else if (biddyManagerType == BIDDYTYPETZBDD) {
536  /* IMPLEMENTED */
537  }
538 #endif
539  else {
540  fprintf(stderr,"Biddy_Managed_IsSmaller: Unsupported BDD type!\n");
541  return FALSE;
542  }
543 
544  return BiddyIsSmaller(biddyOrderingTable,fv,gv);
545 }
546 
547 #ifdef __cplusplus
548 }
549 #endif
550 
551 /***************************************************************************/
562 #ifdef __cplusplus
563 extern "C" {
564 #endif
565 
568 {
569  /* lowest (topmost) variable has global ordering 1 */
570  /* global ordering is the number of zeros in corresponding line of orderingTable */
571 
572  if (!MNG) MNG = biddyAnonymousManager;
573 
574  if (biddyManagerType == BIDDYTYPEOBDD) {
575  /* IMPLEMENTED */
576  }
577  else if (biddyManagerType == BIDDYTYPEOBDDC) {
578  /* IMPLEMENTED */
579  }
580 #ifndef COMPACT
581  else if (biddyManagerType == BIDDYTYPEZBDD) {
582  /* IMPLEMENTED */
583  }
584  else if (biddyManagerType == BIDDYTYPEZBDDC) {
585  /* IMPLEMENTED */
586  }
587  else if (biddyManagerType == BIDDYTYPETZBDD) {
588  /* IMPLEMENTED */
589  }
590 #endif
591  else {
592  fprintf(stderr,"Biddy_Managed_IsLowest: Unsupported BDD type!\n");
593  return FALSE;
594  }
595 
596  /* FOR OBDDs AND OFDDs: the lowest (topmost) variable always has prev=biddyVariableTable.size */
597  /* FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: the topmost variable always has prev=biddyVariableTable.num */
598 
599  if (v >= biddyVariableTable.num) {
600  return FALSE;
601  } else {
602  return (biddyVariableTable.table[v].prev >= biddyVariableTable.num);
603  }
604 }
605 
606 #ifdef __cplusplus
607 }
608 #endif
609 
610 /***************************************************************************/
621 #ifdef __cplusplus
622 extern "C" {
623 #endif
624 
627 {
628  /* highest (bottommost) variable is '1' and has global ordering numUsedVariables */
629  /* global ordering is the number of zeros in corresponding line of orderingTable */
630 
631  if (!MNG) MNG = biddyAnonymousManager;
632 
633  if (biddyManagerType == BIDDYTYPEOBDD) {
634  /* IMPLEMENTED */
635  }
636  else if (biddyManagerType == BIDDYTYPEOBDDC) {
637  /* IMPLEMENTED */
638  }
639 #ifndef COMPACT
640  else if (biddyManagerType == BIDDYTYPEZBDD) {
641  /* IMPLEMENTED */
642  }
643  else if (biddyManagerType == BIDDYTYPEZBDDC) {
644  /* IMPLEMENTED */
645  }
646  else if (biddyManagerType == BIDDYTYPETZBDD) {
647  /* IMPLEMENTED */
648  }
649 #endif
650  else {
651  fprintf(stderr,"Biddy_Managed_IsHighest: Unsupported BDD type!\n");
652  return FALSE;
653  }
654 
655  /* ALWAYS: the highest (bottommost) variable has next=0 */
656 
657  if ((biddyVariableTable.num == 1) && (v == 0)) return TRUE;
658  if ((v == 0) || (v >= biddyVariableTable.num)) {
659  return FALSE;
660  } else {
661  return (biddyVariableTable.table[v].next == 0);
662  }
663 }
664 
665 #ifdef __cplusplus
666 }
667 #endif
668 
669 /***************************************************************************/
681 #ifdef __cplusplus
682 extern "C" {
683 #endif
684 
685 void
687 {
688  if (!MNG) MNG = biddyAnonymousManager;
689 
690  if (biddyManagerType == BIDDYTYPEOBDD) {
691  /* IMPLEMENTED */
692  }
693  else if (biddyManagerType == BIDDYTYPEOBDDC) {
694  /* IMPLEMENTED */
695  }
696 #ifndef COMPACT
697  else if (biddyManagerType == BIDDYTYPEZBDD) {
698  /* IMPLEMENTED */
699  }
700  else if (biddyManagerType == BIDDYTYPEZBDDC) {
701  /* IMPLEMENTED */
702  }
703  else if (biddyManagerType == BIDDYTYPETZBDD) {
704  /* IMPLEMENTED */
705  }
706 #endif
707  else {
708  fprintf(stderr,"Biddy_Managed_Refresh: Unsupported BDD type!\n");
709  return;
710  }
711 
712  BiddyRefresh(f);
713 }
714 
715 #ifdef __cplusplus
716 }
717 #endif
718 
719 /***************************************************************************/
733 #ifdef __cplusplus
734 extern "C" {
735 #endif
736 
739 {
740  if (!MNG) MNG = biddyAnonymousManager;
741 
742  if (biddyManagerType == BIDDYTYPEOBDD) {
743  /* IMPLEMENTED */
744  }
745  else if (biddyManagerType == BIDDYTYPEOBDDC) {
746  /* IMPLEMENTED */
747  }
748 #ifndef COMPACT
749  else if (biddyManagerType == BIDDYTYPEZBDD) {
750  /* IMPLEMENTED */
751  }
752  else if (biddyManagerType == BIDDYTYPEZBDDC) {
753  /* IMPLEMENTED */
754  }
755  else if (biddyManagerType == BIDDYTYPETZBDD) {
756  /* IMPLEMENTED */
757  }
758 #endif
759  else {
760  fprintf(stderr,"Biddy_Managed_IsOK: Unsupported BDD type!\n");
761  return FALSE;
762  }
763 
764  return BiddyManagedIsOK(MNG,f);
765 }
766 
767 #ifdef __cplusplus
768 }
769 #endif
770 
771 /***************************************************************************/
781 #ifdef __cplusplus
782 extern "C" {
783 #endif
784 
785 int
787 {
788  if (!MNG) MNG = biddyAnonymousManager;
789 
790  if (biddyManagerType == BIDDYTYPEOBDD) {
791  /* IMPLEMENTED */
792  }
793  else if (biddyManagerType == BIDDYTYPEOBDDC) {
794  /* IMPLEMENTED */
795  }
796 #ifndef COMPACT
797  else if (biddyManagerType == BIDDYTYPEZBDD) {
798  /* IMPLEMENTED */
799  }
800  else if (biddyManagerType == BIDDYTYPEZBDDC) {
801  /* IMPLEMENTED */
802  }
803  else if (biddyManagerType == BIDDYTYPETZBDD) {
804  /* IMPLEMENTED */
805  }
806 #endif
807  else {
808  fprintf(stderr,"Biddy_Managed_GetManagerType: Unsupported BDD type!\n");
809  return 0;
810  }
811 
812  return BiddyManagedGetManagerType(MNG);
813 }
814 
815 #ifdef __cplusplus
816 }
817 #endif
818 
819 /***************************************************************************/
829 #ifdef __cplusplus
830 extern "C" {
831 #endif
832 
835 {
836  if (!MNG) MNG = biddyAnonymousManager;
837 
838  if (biddyManagerType == BIDDYTYPEOBDD) {
839  /* IMPLEMENTED */
840  }
841  else if (biddyManagerType == BIDDYTYPEOBDDC) {
842  /* IMPLEMENTED */
843  }
844 #ifndef COMPACT
845  else if (biddyManagerType == BIDDYTYPEZBDD) {
846  /* IMPLEMENTED */
847  }
848  else if (biddyManagerType == BIDDYTYPEZBDDC) {
849  /* IMPLEMENTED */
850  }
851  else if (biddyManagerType == BIDDYTYPETZBDD) {
852  /* IMPLEMENTED */
853  }
854 #endif
855  else {
856  fprintf(stderr,"Biddy_Managed_GetManagerName: Unsupported BDD type!\n");
857  return 0;
858  }
859 
860  return BiddyManagedGetManagerName(MNG);
861 }
862 
863 #ifdef __cplusplus
864 }
865 #endif
866 
867 /***************************************************************************/
894 #ifdef __cplusplus
895 extern "C" {
896 #endif
897 
898 void
900  float gcrX, float rr, float rrF, float rrX, float st, float cst)
901 {
902  if (!MNG) MNG = biddyAnonymousManager;
903 
904  if (biddyManagerType == BIDDYTYPEOBDD) {
905  /* IMPLEMENTED */
906  }
907  else if (biddyManagerType == BIDDYTYPEOBDDC) {
908  /* IMPLEMENTED */
909  }
910 #ifndef COMPACT
911  else if (biddyManagerType == BIDDYTYPEZBDD) {
912  /* IMPLEMENTED */
913  }
914  else if (biddyManagerType == BIDDYTYPEZBDDC) {
915  /* IMPLEMENTED */
916  }
917  else if (biddyManagerType == BIDDYTYPETZBDD) {
918  /* IMPLEMENTED */
919  }
920 #endif
921  else {
922  fprintf(stderr,"Biddy_Managed_SetManagerParameters: Unsupported BDD type!\n");
923  return;
924  }
925 
926  BiddyManagedSetManagerParameters(MNG,gcr,gcrF,gcrX,rr,rrF,rrX,st,cst);
927 }
928 
929 #ifdef __cplusplus
930 }
931 #endif
932 
933 /***************************************************************************/
943 #ifdef __cplusplus
944 extern "C" {
945 #endif
946 
949 {
950  Biddy_Edge r;
951 
952  if (!MNG) MNG = biddyAnonymousManager;
953 
954  r = biddyNull;
955 
956  if (biddyManagerType == BIDDYTYPEOBDD) {
957  /* IMPLEMENTED */
958  r = BiddyManagedGetBaseSet(MNG);
959  BiddyRefresh(r); /* not always refreshed by BiddyManagedGetBaseSet */
960  }
961  else if (biddyManagerType == BIDDYTYPEOBDDC) {
962  /* IMPLEMENTED */
963  r = BiddyManagedGetBaseSet(MNG);
964  BiddyRefresh(r); /* not always refreshed by BiddyManagedGetBaseSet */
965  }
966 #ifndef COMPACT
967  else if (biddyManagerType == BIDDYTYPEZBDD) {
968  /* IMPLEMENTED */
969  r = BiddyManagedGetBaseSet(MNG);
970  /* BiddyRefresh() */ /* not needed, because terminal node is returned */
971  }
972  else if (biddyManagerType == BIDDYTYPEZBDDC) {
973  /* IMPLEMENTED */
974  r = BiddyManagedGetBaseSet(MNG);
975  /* BiddyRefresh() */ /* not needed, because terminal node is returned */
976  }
977  else if (biddyManagerType == BIDDYTYPETZBDD) {
978  /* IMPLEMENTED */
979  r = BiddyManagedGetBaseSet(MNG);
980  /* BiddyRefresh() */ /* not needed, because terminal node is returned */
981  }
982 #endif
983  else {
984  fprintf(stderr,"Biddy_Managed_GetBaseSet: Unsupported BDD type!\n");
985  return biddyNull;
986  }
987 
988  return r;
989 }
990 
991 #ifdef __cplusplus
992 }
993 #endif
994 
995 /***************************************************************************/
1010 #ifdef __cplusplus
1011 extern "C" {
1012 #endif
1013 
1014 Biddy_Edge
1016  Biddy_Boolean leftright)
1017 {
1018  if (!MNG) MNG = biddyAnonymousManager;
1019 
1020  if (biddyManagerType == BIDDYTYPEOBDD) {
1021  /* IMPLEMENTED */
1022  }
1023  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1024  /* IMPLEMENTED */
1025  }
1026 #ifndef COMPACT
1027  else if (biddyManagerType == BIDDYTYPEZBDD) {
1028  /* IMPLEMENTED */
1029  }
1030  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1031  /* IMPLEMENTED */
1032  }
1033  else if (biddyManagerType == BIDDYTYPETZBDD) {
1034  /* IMPLEMENTED */
1035  }
1036 #endif
1037  else {
1038  fprintf(stderr,"Biddy_Managed_TransferMark: Unsupported BDD type!\n");
1039  return biddyNull;
1040  }
1041 
1042  return BiddyManagedTransferMark(MNG,f,mark,leftright);
1043 }
1044 
1045 #ifdef __cplusplus
1046 }
1047 #endif
1048 
1049 /***************************************************************************/
1059 #ifdef __cplusplus
1060 extern "C" {
1061 #endif
1062 
1065  Biddy_Edge f2)
1066 {
1067  if (!MNG1) MNG1 = biddyAnonymousManager;
1068 
1069  if (biddyManagerType1 == BIDDYTYPEOBDD) {
1070  /* IMPLEMENTED */
1071  }
1072  else if (biddyManagerType1 == BIDDYTYPEOBDDC) {
1073  /* IMPLEMENTED */
1074  }
1075 #ifndef COMPACT
1076  else if (biddyManagerType1 == BIDDYTYPEZBDD) {
1077  /* IMPLEMENTED */
1078  }
1079  else if (biddyManagerType1 == BIDDYTYPEZBDDC) {
1080  /* IMPLEMENTED */
1081  }
1082  else if (biddyManagerType1 == BIDDYTYPETZBDD) {
1083  /* IMPLEMENTED */
1084  }
1085 #endif
1086  else {
1087  fprintf(stderr,"Biddy_Managed_IsEqv: Unsupported BDD type!\n");
1088  return 0;
1089  }
1090 
1091  if (biddyManagerType2 == BIDDYTYPEOBDD) {
1092  /* IMPLEMENTED */
1093  }
1094  else if (biddyManagerType2 == BIDDYTYPEOBDDC) {
1095  /* IMPLEMENTED */
1096  }
1097 #ifndef COMPACT
1098  else if (biddyManagerType2 == BIDDYTYPEZBDD) {
1099  /* IMPLEMENTED */
1100  }
1101  else if (biddyManagerType2 == BIDDYTYPEZBDDC) {
1102  /* IMPLEMENTED */
1103  }
1104  else if (biddyManagerType2 == BIDDYTYPETZBDD) {
1105  /* IMPLEMENTED */
1106  }
1107 #endif
1108  else {
1109  fprintf(stderr,"Biddy_Managed_IsEqv: Unsupported BDD type!\n");
1110  return 0;
1111  }
1112 
1113  return BiddyManagedIsEqv(MNG1,f1,MNG2,f2);
1114 }
1115 
1116 #ifdef __cplusplus
1117 }
1118 #endif
1119 
1120 /***************************************************************************/
1130 #ifdef __cplusplus
1131 extern "C" {
1132 #endif
1133 
1134 void
1136 {
1137  if (!MNG) MNG = biddyAnonymousManager;
1138 
1139  if (biddyManagerType == BIDDYTYPEOBDD) {
1140  /* IMPLEMENTED */
1141  }
1142  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1143  /* IMPLEMENTED */
1144  }
1145 #ifndef COMPACT
1146  else if (biddyManagerType == BIDDYTYPEZBDD) {
1147  /* IMPLEMENTED */
1148  }
1149  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1150  /* IMPLEMENTED */
1151  }
1152  else if (biddyManagerType == BIDDYTYPETZBDD) {
1153  /* IMPLEMENTED */
1154  }
1155 #endif
1156  else {
1157  fprintf(stderr,"Biddy_Managed_SelectNode: Unsupported BDD type!\n");
1158  return;
1159  }
1160 
1161  BiddyManagedSelectNode(MNG,f);
1162 }
1163 
1164 #ifdef __cplusplus
1165 }
1166 #endif
1167 
1168 /***************************************************************************/
1178 #ifdef __cplusplus
1179 extern "C" {
1180 #endif
1181 
1182 void
1184 {
1185  if (!MNG) MNG = biddyAnonymousManager;
1186 
1187  if (biddyManagerType == BIDDYTYPEOBDD) {
1188  /* IMPLEMENTED */
1189  }
1190  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1191  /* IMPLEMENTED */
1192  }
1193 #ifndef COMPACT
1194  else if (biddyManagerType == BIDDYTYPEZBDD) {
1195  /* IMPLEMENTED */
1196  }
1197  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1198  /* IMPLEMENTED */
1199  }
1200  else if (biddyManagerType == BIDDYTYPETZBDD) {
1201  /* IMPLEMENTED */
1202  }
1203 #endif
1204  else {
1205  fprintf(stderr,"Biddy_Managed_DeselectNode: Unsupported BDD type!\n");
1206  return;
1207  }
1208 
1209  BiddyManagedDeselectNode(MNG,f);
1210 }
1211 
1212 #ifdef __cplusplus
1213 }
1214 #endif
1215 
1216 /***************************************************************************/
1226 #ifdef __cplusplus
1227 extern "C" {
1228 #endif
1229 
1232 {
1233  if (!MNG) MNG = biddyAnonymousManager;
1234 
1235  if (biddyManagerType == BIDDYTYPEOBDD) {
1236  /* IMPLEMENTED */
1237  }
1238  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1239  /* IMPLEMENTED */
1240  }
1241 #ifndef COMPACT
1242  else if (biddyManagerType == BIDDYTYPEZBDD) {
1243  /* IMPLEMENTED */
1244  }
1245  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1246  /* IMPLEMENTED */
1247  }
1248  else if (biddyManagerType == BIDDYTYPETZBDD) {
1249  /* IMPLEMENTED */
1250  }
1251 #endif
1252  else {
1253  fprintf(stderr,"Biddy_Managed_IsSelected: Unsupported BDD type!\n");
1254  return FALSE;
1255  }
1256 
1257  return BiddyManagedIsSelected(MNG,f);
1258 }
1259 
1260 #ifdef __cplusplus
1261 }
1262 #endif
1263 
1264 /***************************************************************************/
1275 #ifdef __cplusplus
1276 extern "C" {
1277 #endif
1278 
1279 void
1281 {
1282  if (!MNG) MNG = biddyAnonymousManager;
1283 
1284  if (biddyManagerType == BIDDYTYPEOBDD) {
1285  /* IMPLEMENTED */
1286  }
1287  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1288  /* IMPLEMENTED */
1289  }
1290 #ifndef COMPACT
1291  else if (biddyManagerType == BIDDYTYPEZBDD) {
1292  /* IMPLEMENTED */
1293  }
1294  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1295  /* IMPLEMENTED */
1296  }
1297  else if (biddyManagerType == BIDDYTYPETZBDD) {
1298  /* IMPLEMENTED */
1299  }
1300 #endif
1301  else {
1302  fprintf(stderr,"Biddy_Managed_SelectFunction: Unsupported BDD type!\n");
1303  return;
1304  }
1305 
1306  BiddyManagedSelectFunction(MNG,f);
1307 }
1308 
1309 #ifdef __cplusplus
1310 }
1311 #endif
1312 
1313 /***************************************************************************/
1323 #ifdef __cplusplus
1324 extern "C" {
1325 #endif
1326 
1327 void
1329 {
1330  if (!MNG) MNG = biddyAnonymousManager;
1331 
1332  if (biddyManagerType == BIDDYTYPEOBDD) {
1333  /* IMPLEMENTED */
1334  }
1335  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1336  /* IMPLEMENTED */
1337  }
1338 #ifndef COMPACT
1339  else if (biddyManagerType == BIDDYTYPEZBDD) {
1340  /* IMPLEMENTED */
1341  }
1342  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1343  /* IMPLEMENTED */
1344  }
1345  else if (biddyManagerType == BIDDYTYPETZBDD) {
1346  /* IMPLEMENTED */
1347  }
1348 #endif
1349  else {
1350  fprintf(stderr,"Biddy_Managed_DeselectAll: Unsupported BDD type!\n");
1351  return;
1352  }
1353 
1354  BiddyManagedDeselectAll(MNG);
1355 }
1356 
1357 #ifdef __cplusplus
1358 }
1359 #endif
1360 
1361 /***************************************************************************/
1372 #ifdef __cplusplus
1373 extern "C" {
1374 #endif
1375 
1378 {
1379  if (!MNG) MNG = biddyAnonymousManager;
1380 
1381  if (biddyManagerType == BIDDYTYPEOBDD) {
1382  /* IMPLEMENTED */
1383  }
1384  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1385  /* IMPLEMENTED */
1386  }
1387 #ifndef COMPACT
1388  else if (biddyManagerType == BIDDYTYPEZBDD) {
1389  /* IMPLEMENTED */
1390  }
1391  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1392  /* IMPLEMENTED */
1393  }
1394  else if (biddyManagerType == BIDDYTYPETZBDD) {
1395  /* IMPLEMENTED */
1396  }
1397 #endif
1398  else {
1399  fprintf(stderr,"Biddy_Managed_GetVariable: Unsupported BDD type!\n");
1400  return 0;
1401  }
1402 
1403  return BiddyManagedGetVariable(MNG,x);
1404 }
1405 
1406 #ifdef __cplusplus
1407 }
1408 #endif
1409 
1410 /***************************************************************************/
1421 #ifdef __cplusplus
1422 extern "C" {
1423 #endif
1424 
1427 {
1428  if (!MNG) MNG = biddyAnonymousManager;
1429 
1430  if (biddyManagerType == BIDDYTYPEOBDD) {
1431  /* IMPLEMENTED */
1432  }
1433  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1434  /* IMPLEMENTED */
1435  }
1436 #ifndef COMPACT
1437  else if (biddyManagerType == BIDDYTYPEZBDD) {
1438  /* IMPLEMENTED */
1439  }
1440  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1441  /* IMPLEMENTED */
1442  }
1443  else if (biddyManagerType == BIDDYTYPETZBDD) {
1444  /* IMPLEMENTED */
1445  }
1446 #endif
1447  else {
1448  fprintf(stderr,"Biddy_Managed_GetLowestVariable: Unsupported BDD type!\n");
1449  return 0;
1450  }
1451 
1452  return BiddyManagedGetLowestVariable(MNG);
1453 }
1454 
1455 #ifdef __cplusplus
1456 }
1457 #endif
1458 
1459 /***************************************************************************/
1474 #ifdef __cplusplus
1475 extern "C" {
1476 #endif
1477 
1480 {
1481  if (!MNG) MNG = biddyAnonymousManager;
1482 
1483  if (biddyManagerType == BIDDYTYPEOBDD) {
1484  /* IMPLEMENTED */
1485  }
1486  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1487  /* IMPLEMENTED */
1488  }
1489 #ifndef COMPACT
1490  else if (biddyManagerType == BIDDYTYPEZBDD) {
1491  /* IMPLEMENTED */
1492  }
1493  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1494  /* IMPLEMENTED */
1495  }
1496  else if (biddyManagerType == BIDDYTYPETZBDD) {
1497  /* IMPLEMENTED */
1498  }
1499 #endif
1500  else {
1501  fprintf(stderr,"Biddy_Managed_GetIthVariable: Unsupported BDD type!\n");
1502  return 0;
1503  }
1504 
1505  return BiddyManagedGetIthVariable(MNG,i);
1506 }
1507 
1508 #ifdef __cplusplus
1509 }
1510 #endif
1511 
1512 /***************************************************************************/
1522 #ifdef __cplusplus
1523 extern "C" {
1524 #endif
1525 
1528 {
1529  if (!MNG) MNG = biddyAnonymousManager;
1530 
1531  if (biddyManagerType == BIDDYTYPEOBDD) {
1532  /* IMPLEMENTED */
1533  }
1534  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1535  /* IMPLEMENTED */
1536  }
1537 #ifndef COMPACT
1538  else if (biddyManagerType == BIDDYTYPEZBDD) {
1539  /* IMPLEMENTED */
1540  }
1541  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1542  /* IMPLEMENTED */
1543  }
1544  else if (biddyManagerType == BIDDYTYPETZBDD) {
1545  /* IMPLEMENTED */
1546  }
1547 #endif
1548  else {
1549  fprintf(stderr,"Biddy_Managed_GetPrevVariable: Unsupported BDD type!\n");
1550  return 0;
1551  }
1552 
1553  return BiddyManagedGetPrevVariable(MNG,v);
1554 }
1555 
1556 #ifdef __cplusplus
1557 }
1558 #endif
1559 
1560 /***************************************************************************/
1570 #ifdef __cplusplus
1571 extern "C" {
1572 #endif
1573 
1576 {
1577  if (!MNG) MNG = biddyAnonymousManager;
1578 
1579  if (biddyManagerType == BIDDYTYPEOBDD) {
1580  /* IMPLEMENTED */
1581  }
1582  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1583  /* IMPLEMENTED */
1584  }
1585 #ifndef COMPACT
1586  else if (biddyManagerType == BIDDYTYPEZBDD) {
1587  /* IMPLEMENTED */
1588  }
1589  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1590  /* IMPLEMENTED */
1591  }
1592  else if (biddyManagerType == BIDDYTYPETZBDD) {
1593  /* IMPLEMENTED */
1594  }
1595 #endif
1596  else {
1597  fprintf(stderr,"Biddy_Managed_GetNextVariable: Unsupported BDD type!\n");
1598  return 0;
1599  }
1600 
1601  return BiddyManagedGetNextVariable(MNG,v);
1602 }
1603 
1604 #ifdef __cplusplus
1605 }
1606 #endif
1607 
1608 /***************************************************************************/
1617 #ifdef __cplusplus
1618 extern "C" {
1619 #endif
1620 
1621 Biddy_Edge
1623 {
1624  if (!MNG) MNG = biddyAnonymousManager;
1625 
1626  if (biddyManagerType == BIDDYTYPEOBDD) {
1627  /* IMPLEMENTED */
1628  }
1629  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1630  /* IMPLEMENTED */
1631  }
1632 #ifndef COMPACT
1633  else if (biddyManagerType == BIDDYTYPEZBDD) {
1634  /* IMPLEMENTED */
1635  }
1636  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1637  /* IMPLEMENTED */
1638  }
1639  else if (biddyManagerType == BIDDYTYPETZBDD) {
1640  /* IMPLEMENTED */
1641  }
1642 #endif
1643  else {
1644  fprintf(stderr,"Biddy_Managed_GetVariableEdge: Unsupported BDD type!\n");
1645  return biddyNull;
1646  }
1647 
1648  return BiddyManagedGetVariableEdge(MNG,v);
1649 }
1650 
1651 #ifdef __cplusplus
1652 }
1653 #endif
1654 
1655 /***************************************************************************/
1664 #ifdef __cplusplus
1665 extern "C" {
1666 #endif
1667 
1668 Biddy_Edge
1670 {
1671  if (!MNG) MNG = biddyAnonymousManager;
1672 
1673  if (biddyManagerType == BIDDYTYPEOBDD) {
1674  /* IMPLEMENTED */
1675  }
1676  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1677  /* IMPLEMENTED */
1678  }
1679 #ifndef COMPACT
1680  else if (biddyManagerType == BIDDYTYPEZBDD) {
1681  /* IMPLEMENTED */
1682  }
1683  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1684  /* IMPLEMENTED */
1685  }
1686  else if (biddyManagerType == BIDDYTYPETZBDD) {
1687  /* IMPLEMENTED */
1688  }
1689 #endif
1690  else {
1691  fprintf(stderr,"Biddy_Managed_GetElementEdge: Unsupported BDD type!\n");
1692  return biddyNull;
1693  }
1694 
1695  return BiddyManagedGetElementEdge(MNG,v);
1696 }
1697 
1698 #ifdef __cplusplus
1699 }
1700 #endif
1701 
1702 /***************************************************************************/
1711 #ifdef __cplusplus
1712 extern "C" {
1713 #endif
1714 
1717 {
1718  if (!MNG) MNG = biddyAnonymousManager;
1719 
1720  if (biddyManagerType == BIDDYTYPEOBDD) {
1721  /* IMPLEMENTED */
1722  }
1723  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1724  /* IMPLEMENTED */
1725  }
1726 #ifndef COMPACT
1727  else if (biddyManagerType == BIDDYTYPEZBDD) {
1728  /* IMPLEMENTED */
1729  }
1730  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1731  /* IMPLEMENTED */
1732  }
1733  else if (biddyManagerType == BIDDYTYPETZBDD) {
1734  /* IMPLEMENTED */
1735  }
1736 #endif
1737  else {
1738  fprintf(stderr,"Biddy_Managed_GetVariableName: Unsupported BDD type!\n");
1739  return NULL;
1740  }
1741 
1742  return BiddyManagedGetVariableName(MNG,v);
1743 }
1744 
1745 #ifdef __cplusplus
1746 }
1747 #endif
1748 
1749 /***************************************************************************/
1761 #ifdef __cplusplus
1762 extern "C" {
1763 #endif
1764 
1765 Biddy_Edge
1767 {
1768  if (!MNG) MNG = biddyAnonymousManager;
1769 
1770  if (biddyManagerType == BIDDYTYPEOBDD) {
1771  /* IMPLEMENTED */
1772  }
1773  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1774  /* IMPLEMENTED */
1775  }
1776 #ifndef COMPACT
1777  else if (biddyManagerType == BIDDYTYPEZBDD) {
1778  /* IMPLEMENTED */
1779  }
1780  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1781  /* IMPLEMENTED */
1782  }
1783  else if (biddyManagerType == BIDDYTYPETZBDD) {
1784  /* IMPLEMENTED */
1785  }
1786 #endif
1787  else {
1788  fprintf(stderr,"Biddy_Managed_GetTopVariableEdge: Unsupported BDD type!\n");
1789  return biddyNull;
1790  }
1791 
1792  return BiddyManagedGetTopVariableEdge(MNG,f);
1793 }
1794 
1795 #ifdef __cplusplus
1796 }
1797 #endif
1798 
1799 /***************************************************************************/
1809 #ifdef __cplusplus
1810 extern "C" {
1811 #endif
1812 
1815 {
1816  if (!MNG) MNG = biddyAnonymousManager;
1817 
1818  if (biddyManagerType == BIDDYTYPEOBDD) {
1819  /* IMPLEMENTED */
1820  }
1821  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1822  /* IMPLEMENTED */
1823  }
1824 #ifndef COMPACT
1825  else if (biddyManagerType == BIDDYTYPEZBDD) {
1826  /* IMPLEMENTED */
1827  }
1828  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1829  /* IMPLEMENTED */
1830  }
1831  else if (biddyManagerType == BIDDYTYPETZBDD) {
1832  /* IMPLEMENTED */
1833  }
1834 #endif
1835  else {
1836  fprintf(stderr,"Biddy_Managed_GetTopVariableName: Unsupported BDD type!\n");
1837  return NULL;
1838  }
1839 
1840  return BiddyManagedGetTopVariableName(MNG,f);
1841 }
1842 
1843 #ifdef __cplusplus
1844 }
1845 #endif
1846 
1847 /***************************************************************************/
1857 #ifdef __cplusplus
1858 extern "C" {
1859 #endif
1860 
1861 char
1863 {
1864  if (!MNG) MNG = biddyAnonymousManager;
1865 
1866  if (biddyManagerType == BIDDYTYPEOBDD) {
1867  /* IMPLEMENTED */
1868  }
1869  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1870  /* IMPLEMENTED */
1871  }
1872 #ifndef COMPACT
1873  else if (biddyManagerType == BIDDYTYPEZBDD) {
1874  /* IMPLEMENTED */
1875  }
1876  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1877  /* IMPLEMENTED */
1878  }
1879  else if (biddyManagerType == BIDDYTYPETZBDD) {
1880  /* IMPLEMENTED */
1881  }
1882 #endif
1883  else {
1884  fprintf(stderr,"Biddy_Managed_GetTopVariableChar: Unsupported BDD type!\n");
1885  return 0;
1886  }
1887 
1888  return BiddyManagedGetTopVariableChar(MNG,f);
1889 }
1890 
1891 #ifdef __cplusplus
1892 }
1893 #endif
1894 
1895 /***************************************************************************/
1906 #ifdef __cplusplus
1907 extern "C" {
1908 #endif
1909 
1910 void
1912 {
1913  if (!MNG) MNG = biddyAnonymousManager;
1914 
1915  if (biddyManagerType == BIDDYTYPEOBDD) {
1916  /* IMPLEMENTED */
1917  }
1918  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1919  /* IMPLEMENTED */
1920  }
1921 #ifndef COMPACT
1922  else if (biddyManagerType == BIDDYTYPEZBDD) {
1923  /* IMPLEMENTED */
1924  }
1925  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1926  /* IMPLEMENTED */
1927  }
1928  else if (biddyManagerType == BIDDYTYPETZBDD) {
1929  /* IMPLEMENTED */
1930  }
1931 #endif
1932  else {
1933  fprintf(stderr,"Biddy_Managed_ResetVariablesValue: Unsupported BDD type!\n");
1934  return;
1935  }
1936 
1937  BiddyManagedResetVariablesValue(MNG);
1938 }
1939 
1940 #ifdef __cplusplus
1941 }
1942 #endif
1943 
1944 /***************************************************************************/
1954 #ifdef __cplusplus
1955 extern "C" {
1956 #endif
1957 
1958 void
1960 {
1961  if (!MNG) MNG = biddyAnonymousManager;
1962 
1963  if (biddyManagerType == BIDDYTYPEOBDD) {
1964  /* IMPLEMENTED */
1965  }
1966  else if (biddyManagerType == BIDDYTYPEOBDDC) {
1967  /* IMPLEMENTED */
1968  }
1969 #ifndef COMPACT
1970  else if (biddyManagerType == BIDDYTYPEZBDD) {
1971  /* IMPLEMENTED */
1972  }
1973  else if (biddyManagerType == BIDDYTYPEZBDDC) {
1974  /* IMPLEMENTED */
1975  }
1976  else if (biddyManagerType == BIDDYTYPETZBDD) {
1977  /* IMPLEMENTED */
1978  }
1979 #endif
1980  else {
1981  fprintf(stderr,"Biddy_Managed_SetVariableValue: Unsupported BDD type!\n");
1982  return;
1983  }
1984 
1985  BiddyManagedSetVariableValue(MNG,v,f);
1986 }
1987 
1988 #ifdef __cplusplus
1989 }
1990 #endif
1991 
1992 /***************************************************************************/
2002 #ifdef __cplusplus
2003 extern "C" {
2004 #endif
2005 
2006 Biddy_Edge
2008 {
2009  if (!MNG) MNG = biddyAnonymousManager;
2010 
2011  if (biddyManagerType == BIDDYTYPEOBDD) {
2012  /* IMPLEMENTED */
2013  }
2014  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2015  /* IMPLEMENTED */
2016  }
2017 #ifndef COMPACT
2018  else if (biddyManagerType == BIDDYTYPEZBDD) {
2019  /* IMPLEMENTED */
2020  }
2021  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2022  /* IMPLEMENTED */
2023  }
2024  else if (biddyManagerType == BIDDYTYPETZBDD) {
2025  /* IMPLEMENTED */
2026  }
2027 #endif
2028  else {
2029  fprintf(stderr,"Biddy_Managed_GetVariableValue: Unsupported BDD type!\n");
2030  return biddyNull;
2031  }
2032 
2033  return BiddyManagedGetVariableValue(MNG,v);
2034 }
2035 
2036 #ifdef __cplusplus
2037 }
2038 #endif
2039 
2040 /***************************************************************************/
2051 #ifdef __cplusplus
2052 extern "C" {
2053 #endif
2054 
2055 void
2057 {
2058  if (!MNG) MNG = biddyAnonymousManager;
2059 
2060  if (biddyManagerType == BIDDYTYPEOBDD) {
2061  /* IMPLEMENTED */
2062  }
2063  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2064  /* IMPLEMENTED */
2065  }
2066 #ifndef COMPACT
2067  else if (biddyManagerType == BIDDYTYPEZBDD) {
2068  /* IMPLEMENTED */
2069  }
2070  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2071  /* IMPLEMENTED */
2072  }
2073  else if (biddyManagerType == BIDDYTYPETZBDD) {
2074  /* IMPLEMENTED */
2075  }
2076 #endif
2077  else {
2078  fprintf(stderr,"Biddy_Managed_ClearVariablesData: Unsupported BDD type!\n");
2079  return;
2080  }
2081 
2082  BiddyManagedClearVariablesData(MNG);
2083 }
2084 
2085 #ifdef __cplusplus
2086 }
2087 #endif
2088 
2089 /***************************************************************************/
2099 #ifdef __cplusplus
2100 extern "C" {
2101 #endif
2102 
2103 void
2105 {
2106  if (!MNG) MNG = biddyAnonymousManager;
2107 
2108  if (biddyManagerType == BIDDYTYPEOBDD) {
2109  /* IMPLEMENTED */
2110  }
2111  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2112  /* IMPLEMENTED */
2113  }
2114 #ifndef COMPACT
2115  else if (biddyManagerType == BIDDYTYPEZBDD) {
2116  /* IMPLEMENTED */
2117  }
2118  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2119  /* IMPLEMENTED */
2120  }
2121  else if (biddyManagerType == BIDDYTYPETZBDD) {
2122  /* IMPLEMENTED */
2123  }
2124 #endif
2125  else {
2126  fprintf(stderr,"Biddy_Managed_SetVariableData: Unsupported BDD type!\n");
2127  return;
2128  }
2129 
2130  BiddyManagedSetVariableData(MNG,v,x);
2131 }
2132 
2133 #ifdef __cplusplus
2134 }
2135 #endif
2136 
2137 /***************************************************************************/
2147 #ifdef __cplusplus
2148 extern "C" {
2149 #endif
2150 
2151 void *
2153 {
2154  if (!MNG) MNG = biddyAnonymousManager;
2155 
2156  if (biddyManagerType == BIDDYTYPEOBDD) {
2157  /* IMPLEMENTED */
2158  }
2159  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2160  /* IMPLEMENTED */
2161  }
2162 #ifndef COMPACT
2163  else if (biddyManagerType == BIDDYTYPEZBDD) {
2164  /* IMPLEMENTED */
2165  }
2166  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2167  /* IMPLEMENTED */
2168  }
2169  else if (biddyManagerType == BIDDYTYPETZBDD) {
2170  /* IMPLEMENTED */
2171  }
2172 #endif
2173  else {
2174  fprintf(stderr,"Biddy_Managed_GetVariableData: Unsupported BDD type!\n");
2175  return NULL;
2176  }
2177 
2178  return BiddyManagedGetVariableData(MNG,v);
2179 }
2180 
2181 #ifdef __cplusplus
2182 }
2183 #endif
2184 
2185 /***************************************************************************/
2198 #ifdef __cplusplus
2199 extern "C" {
2200 #endif
2201 
2204 {
2205  if (!MNG) MNG = biddyAnonymousManager;
2206 
2207  if (biddyManagerType == BIDDYTYPEOBDD) {
2208  /* IMPLEMENTED */
2209  }
2210  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2211  /* IMPLEMENTED */
2212  }
2213 #ifndef COMPACT
2214  else if (biddyManagerType == BIDDYTYPEZBDD) {
2215  /* IMPLEMENTED */
2216  }
2217  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2218  /* IMPLEMENTED */
2219  }
2220  else if (biddyManagerType == BIDDYTYPETZBDD) {
2221  /* IMPLEMENTED */
2222  }
2223 #endif
2224  else {
2225  fprintf(stderr,"Biddy_Managed_Eval: Unsupported BDD type!\n");
2226  return FALSE;
2227  }
2228 
2229  return BiddyManagedEval(MNG,f);
2230 }
2231 
2232 #ifdef __cplusplus
2233 }
2234 #endif
2235 
2236 /***************************************************************************/
2249 #ifdef __cplusplus
2250 extern "C" {
2251 #endif
2252 
2253 double
2255 {
2256  if (!MNG) MNG = biddyAnonymousManager;
2257 
2258  if (biddyManagerType == BIDDYTYPEOBDD) {
2259  /* IMPLEMENTED */
2260  }
2261  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2262  /* IMPLEMENTED */
2263  }
2264 #ifndef COMPACT
2265  else if (biddyManagerType == BIDDYTYPEZBDD) {
2266  /* IMPLEMENTED */
2267  }
2268  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2269  /* IMPLEMENTED */
2270  }
2271  else if (biddyManagerType == BIDDYTYPETZBDD) {
2272  /* IMPLEMENTED */
2273  }
2274 #endif
2275  else {
2276  fprintf(stderr,"Biddy_Managed_EvalProbability: Unsupported BDD type!\n");
2277  return 0.0;
2278  }
2279 
2280  return BiddyManagedEvalProbability(MNG,f);
2281 }
2282 
2283 #ifdef __cplusplus
2284 }
2285 #endif
2286 
2287 /***************************************************************************/
2324 #ifdef __cplusplus
2325 extern "C" {
2326 #endif
2327 
2330  Biddy_Boolean varelem)
2331 {
2332  if (!MNG) MNG = biddyAnonymousManager;
2333 
2334  if (biddyManagerType == BIDDYTYPEOBDD) {
2335  /* IMPLEMENTED */
2336  }
2337  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2338  /* IMPLEMENTED */
2339  }
2340 #ifndef COMPACT
2341  else if (biddyManagerType == BIDDYTYPEZBDD) {
2342  /* IMPLEMENTED */
2343  }
2344  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2345  /* IMPLEMENTED */
2346  }
2347  else if (biddyManagerType == BIDDYTYPETZBDD) {
2348  /* IMPLEMENTED */
2349  }
2350 #endif
2351  else {
2352  fprintf(stderr,"Biddy_Managed_FoaVariable: Unsupported BDD type!\n");
2353  return 0;
2354  }
2355 
2356  return BiddyManagedFoaVariable(MNG,x,varelem,TRUE);
2357 }
2358 
2359 #ifdef __cplusplus
2360 }
2361 #endif
2362 
2363 /***************************************************************************/
2376 #ifdef __cplusplus
2377 extern "C" {
2378 #endif
2379 
2380 void
2382 {
2383  if (!MNG) MNG = biddyAnonymousManager;
2384 
2385  if (biddyManagerType == BIDDYTYPEOBDD) {
2386  /* IMPLEMENTED */
2387  }
2388  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2389  /* IMPLEMENTED */
2390  }
2391 #ifndef COMPACT
2392  else if (biddyManagerType == BIDDYTYPEZBDD) {
2393  /* IMPLEMENTED */
2394  }
2395  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2396  /* IMPLEMENTED */
2397  }
2398  else if (biddyManagerType == BIDDYTYPETZBDD) {
2399  /* IMPLEMENTED */
2400  }
2401 #endif
2402  else {
2403  fprintf(stderr,"Biddy_Managed_ChangeVariableName: Unsupported BDD type!\n");
2404  return;
2405  }
2406 
2407  BiddyManagedChangeVariableName(MNG,v,x);
2408 }
2409 
2410 #ifdef __cplusplus
2411 }
2412 #endif
2413 
2414 /***************************************************************************/
2429 #ifdef __cplusplus
2430 extern "C" {
2431 #endif
2432 
2435 {
2436  if (!MNG) MNG = biddyAnonymousManager;
2437 
2438  if (biddyManagerType == BIDDYTYPEOBDD) {
2439  /* IMPLEMENTED */
2440  }
2441  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2442  /* IMPLEMENTED */
2443  }
2444 #ifndef COMPACT
2445  else if (biddyManagerType == BIDDYTYPEZBDD) {
2446  /* IMPLEMENTED */
2447  }
2448  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2449  /* IMPLEMENTED */
2450  }
2451  else if (biddyManagerType == BIDDYTYPETZBDD) {
2452  /* IMPLEMENTED */
2453  }
2454 #endif
2455  else {
2456  fprintf(stderr,"Biddy_Managed_AddVariableByName: Unsupported BDD type!\n");
2457  return 0;
2458  }
2459 
2460  return BiddyManagedAddVariableByName(MNG,x);
2461 }
2462 
2463 #ifdef __cplusplus
2464 }
2465 #endif
2466 
2467 /***************************************************************************/
2482 #ifdef __cplusplus
2483 extern "C" {
2484 #endif
2485 
2488 {
2489  if (!MNG) MNG = biddyAnonymousManager;
2490 
2491  if (biddyManagerType == BIDDYTYPEOBDD) {
2492  /* IMPLEMENTED */
2493  }
2494  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2495  /* IMPLEMENTED */
2496  }
2497 #ifndef COMPACT
2498  else if (biddyManagerType == BIDDYTYPEZBDD) {
2499  /* IMPLEMENTED */
2500  }
2501  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2502  /* IMPLEMENTED */
2503  }
2504  else if (biddyManagerType == BIDDYTYPETZBDD) {
2505  /* IMPLEMENTED */
2506  }
2507 #endif
2508  else {
2509  fprintf(stderr,"Biddy_Managed_AddElementByName: Unsupported BDD type!\n");
2510  return 0;
2511  }
2512 
2513  return BiddyManagedAddElementByName(MNG,x);
2514 }
2515 
2516 #ifdef __cplusplus
2517 }
2518 #endif
2519 
2520 /***************************************************************************/
2533 #ifdef __cplusplus
2534 extern "C" {
2535 #endif
2536 
2537 Biddy_Edge
2539 {
2540  if (!MNG) MNG = biddyAnonymousManager;
2541 
2542  if (biddyManagerType == BIDDYTYPEOBDD) {
2543  /* IMPLEMENTED */
2544  }
2545  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2546  /* IMPLEMENTED */
2547  }
2548 #ifndef COMPACT
2549  else if (biddyManagerType == BIDDYTYPEZBDD) {
2550  /* IMPLEMENTED */
2551  }
2552  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2553  /* IMPLEMENTED */
2554  }
2555  else if (biddyManagerType == BIDDYTYPETZBDD) {
2556  /* IMPLEMENTED */
2557  }
2558 #endif
2559  else {
2560  fprintf(stderr,"Biddy_Managed_AddVariableBelow: Unsupported BDD type!\n");
2561  return biddyNull;
2562  }
2563 
2564  return BiddyManagedAddVariableBelow(MNG,v);
2565 }
2566 
2567 #ifdef __cplusplus
2568 }
2569 #endif
2570 
2571 /***************************************************************************/
2584 #ifdef __cplusplus
2585 extern "C" {
2586 #endif
2587 
2588 Biddy_Edge
2590 {
2591  if (!MNG) MNG = biddyAnonymousManager;
2592 
2593  if (biddyManagerType == BIDDYTYPEOBDD) {
2594  /* IMPLEMENTED */
2595  }
2596  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2597  /* IMPLEMENTED */
2598  }
2599 #ifndef COMPACT
2600  else if (biddyManagerType == BIDDYTYPEZBDD) {
2601  /* IMPLEMENTED */
2602  }
2603  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2604  /* IMPLEMENTED */
2605  }
2606  else if (biddyManagerType == BIDDYTYPETZBDD) {
2607  /* IMPLEMENTED */
2608  }
2609 #endif
2610  else {
2611  fprintf(stderr,"Biddy_Managed_AddVariableAbove: Unsupported BDD type!\n");
2612  return biddyNull;
2613  }
2614 
2615  return BiddyManagedAddVariableAbove(MNG,v);
2616 }
2617 
2618 #ifdef __cplusplus
2619 }
2620 #endif
2621 
2622 /***************************************************************************/
2634 #ifdef __cplusplus
2635 extern "C" {
2636 #endif
2637 
2638 Biddy_Edge
2640 {
2641  if (!MNG) MNG = biddyAnonymousManager;
2642 
2643  if (biddyManagerType == BIDDYTYPEOBDD) {
2644  /* IMPLEMENTED */
2645  }
2646  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2647  /* IMPLEMENTED */
2648  }
2649 #ifndef COMPACT
2650  else if (biddyManagerType == BIDDYTYPEZBDD) {
2651  /* IMPLEMENTED */
2652  }
2653  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2654  /* IMPLEMENTED */
2655  }
2656  else if (biddyManagerType == BIDDYTYPETZBDD) {
2657  /* IMPLEMENTED */
2658  }
2659  else if (biddyManagerType == BIDDYTYPETZBDDC) {
2660  /* NOT IMPLEMENTED, YET */
2661  fprintf(stderr,"Biddy_Managed_IncTag: this BDD type is not supported, yet!\n");
2662  return biddyNull;
2663  }
2664 #endif
2665  else {
2666  fprintf(stderr,"Biddy_Managed_IncTag: Unsupported BDD type!\n");
2667  return biddyNull;
2668  }
2669 
2670  return BiddyManagedIncTag(MNG,f);
2671 }
2672 
2673 #ifdef __cplusplus
2674 }
2675 #endif
2676 
2677 /***************************************************************************/
2706 #ifdef __cplusplus
2707 extern "C" {
2708 #endif
2709 
2710 Biddy_Edge
2712  Biddy_Edge pt, Biddy_Variable ptag,
2713  Biddy_Boolean garbageAllowed)
2714 {
2715  Biddy_Edge r;
2716 
2717  if (!MNG) MNG = biddyAnonymousManager;
2718 
2719  assert( (pf == NULL) || (BiddyIsOK(pf) == TRUE) );
2720  assert( (pt == NULL) || (BiddyIsOK(pt) == TRUE) );
2721 
2722  r = biddyNull;
2723 
2724  if (biddyManagerType == BIDDYTYPEOBDD) {
2725  /* IMPLEMENTED */
2726  r = BiddyManagedTaggedFoaNode(MNG,v,pf,pt,ptag,garbageAllowed);
2727  BiddyRefresh(r); /* BiddyManagedTaggedFoaNode returns an obsolete node! */
2728  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
2729  /* IMPLEMENTED */
2730  r = BiddyManagedTaggedFoaNode(MNG,v,pf,pt,ptag,garbageAllowed);
2731  BiddyRefresh(r); /* BiddyManagedTaggedFoaNode returns an obsolete node! */
2732  }
2733 #ifndef COMPACT
2734  else if (biddyManagerType == BIDDYTYPEZBDD) {
2735  /* IMPLEMENTED */
2736  r = BiddyManagedTaggedFoaNode(MNG,v,pf,pt,ptag,garbageAllowed);
2737  BiddyRefresh(r); /* BiddyManagedTaggedFoaNode returns an obsolete node! */
2738  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
2739  /* IMPLEMENTED */
2740  r = BiddyManagedTaggedFoaNode(MNG,v,pf,pt,ptag,garbageAllowed);
2741  BiddyRefresh(r); /* BiddyManagedTaggedFoaNode returns an obsolete node! */
2742  } else if (biddyManagerType == BIDDYTYPETZBDD) {
2743  /* IMPLEMENTED */
2744  r = BiddyManagedTaggedFoaNode(MNG,v,pf,pt,ptag,garbageAllowed);
2745  BiddyRefresh(r); /* BiddyManagedTaggedFoaNode returns an obsolete node! */
2746  } else if (biddyManagerType == BIDDYTYPETZBDDC) {
2747  fprintf(stderr,"Biddy_Managed_TaggedFoaNode: this BDD type is not supported, yet!\n");
2748  return biddyNull;
2749  }
2750 #endif
2751  else {
2752  fprintf(stderr,"Biddy_Managed_TaggedFoaNode: Unsupported BDD type!\n");
2753  return biddyNull;
2754  }
2755 
2756  return r;
2757 }
2758 
2759 #ifdef __cplusplus
2760 }
2761 #endif
2762 
2763 /***************************************************************************/
2799 #ifdef __cplusplus
2800 extern "C" {
2801 #endif
2802 
2803 void
2805  Biddy_Variable targetGEQ, Biddy_Boolean purge,
2806  Biddy_Boolean total)
2807 {
2808  if (!MNG) MNG = biddyAnonymousManager;
2809  ZF_LOGI("Biddy_GC");
2810 
2811  if (biddyManagerType == BIDDYTYPEOBDD) {
2812  /* IMPLEMENTED */
2813  }
2814  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2815  /* IMPLEMENTED */
2816  }
2817 #ifndef COMPACT
2818  else if (biddyManagerType == BIDDYTYPEZBDD) {
2819  /* IMPLEMENTED */
2820  }
2821  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2822  /* IMPLEMENTED */
2823  }
2824  else if (biddyManagerType == BIDDYTYPETZBDD) {
2825  /* IMPLEMENTED */
2826  }
2827 #endif
2828  else {
2829  fprintf(stderr,"Biddy_Managed_GC: Unsupported BDD type!\n");
2830  return;
2831  }
2832 
2833  BiddyManagedGC(MNG,targetLT,targetGEQ,purge,total);
2834 }
2835 
2836 #ifdef __cplusplus
2837 }
2838 #endif
2839 
2840 /***************************************************************************/
2854 #ifdef __cplusplus
2855 extern "C" {
2856 #endif
2857 
2858 void
2860 {
2861  if (!MNG) MNG = biddyAnonymousManager;
2862 
2863  if (biddyManagerType == BIDDYTYPEOBDD) {
2864  /* IMPLEMENTED */
2865  }
2866  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2867  /* IMPLEMENTED */
2868  }
2869 #ifndef COMPACT
2870  else if (biddyManagerType == BIDDYTYPEZBDD) {
2871  /* IMPLEMENTED */
2872  }
2873  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2874  /* IMPLEMENTED */
2875  }
2876  else if (biddyManagerType == BIDDYTYPETZBDD) {
2877  /* IMPLEMENTED */
2878  }
2879 #endif
2880  else {
2881  fprintf(stderr,"Biddy_Managed_Clean: Unsupported BDD type!\n");
2882  return;
2883  }
2884 
2885  BiddyManagedClean(MNG);
2886 }
2887 
2888 #ifdef __cplusplus
2889 }
2890 #endif
2891 
2892 /***************************************************************************/
2910 #ifdef __cplusplus
2911 extern "C" {
2912 #endif
2913 
2914 void
2916 {
2917  if (!MNG) MNG = biddyAnonymousManager;
2918 
2919  if (biddyManagerType == BIDDYTYPEOBDD) {
2920  /* IMPLEMENTED */
2921  }
2922  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2923  /* IMPLEMENTED */
2924  }
2925 #ifndef COMPACT
2926  else if (biddyManagerType == BIDDYTYPEZBDD) {
2927  /* IMPLEMENTED */
2928  }
2929  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2930  /* IMPLEMENTED */
2931  }
2932  else if (biddyManagerType == BIDDYTYPETZBDD) {
2933  /* IMPLEMENTED */
2934  }
2935 #endif
2936  else {
2937  fprintf(stderr,"Biddy_Managed_Purge: Unsupported BDD type!\n");
2938  return;
2939  }
2940 
2941  BiddyManagedPurge(MNG);
2942 }
2943 
2944 #ifdef __cplusplus
2945 }
2946 #endif
2947 
2948 /***************************************************************************/
2966 #ifdef __cplusplus
2967 extern "C" {
2968 #endif
2969 
2970 void
2972  Biddy_Boolean converge)
2973 {
2974  if (!MNG) MNG = biddyAnonymousManager;
2975 
2976  if (biddyManagerType == BIDDYTYPEOBDD) {
2977  /* IMPLEMENTED */
2978  }
2979  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2980  /* IMPLEMENTED */
2981  }
2982 #ifndef COMPACT
2983  else if (biddyManagerType == BIDDYTYPEZBDD) {
2984  /* IMPLEMENTED */
2985  }
2986  else if (biddyManagerType == BIDDYTYPEZBDDC) {
2987  /* IMPLEMENTED */
2988  }
2989  else if (biddyManagerType == BIDDYTYPETZBDD) {
2990  /* IMPLEMENTED */
2991  }
2992 #endif
2993  else {
2994  fprintf(stderr,"Biddy_Managed_PurgeAndReorder: Unsupported BDD type!\n");
2995  return;
2996  }
2997 
2998  BiddyManagedPurgeAndReorder(MNG,f,converge);
2999 }
3000 
3001 #ifdef __cplusplus
3002 }
3003 #endif
3004 
3005 /***************************************************************************/
3015 #ifdef __cplusplus
3016 extern "C" {
3017 #endif
3018 
3019 void
3021 {
3022  if (!MNG) MNG = biddyAnonymousManager;
3023 
3024  if (biddyManagerType == BIDDYTYPEOBDD) {
3025  /* IMPLEMENTED */
3026  }
3027  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3028  /* IMPLEMENTED */
3029  }
3030 #ifndef COMPACT
3031  else if (biddyManagerType == BIDDYTYPEZBDD) {
3032  /* IMPLEMENTED */
3033  }
3034  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3035  /* IMPLEMENTED */
3036  }
3037  else if (biddyManagerType == BIDDYTYPETZBDD) {
3038  /* IMPLEMENTED */
3039  }
3040 #endif
3041  else {
3042  fprintf(stderr,"Biddy_Managed_AddCache: Unsupported BDD type!\n");
3043  return;
3044  }
3045 
3046  BiddyManagedAddCache(MNG,gc);
3047 }
3048 
3049 #ifdef __cplusplus
3050 }
3051 #endif
3052 
3053 /***************************************************************************/
3088 #ifdef __cplusplus
3089 extern "C" {
3090 #endif
3091 
3092 unsigned int
3094 {
3095  if (!MNG) MNG = biddyAnonymousManager;
3096 
3097  if (biddyManagerType == BIDDYTYPEOBDD) {
3098  /* IMPLEMENTED */
3099  }
3100  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3101  /* IMPLEMENTED */
3102  }
3103 #ifndef COMPACT
3104  else if (biddyManagerType == BIDDYTYPEZBDD) {
3105  /* IMPLEMENTED */
3106  }
3107  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3108  /* IMPLEMENTED */
3109  }
3110  else if (biddyManagerType == BIDDYTYPETZBDD) {
3111  /* IMPLEMENTED */
3112  }
3113 #endif
3114  else {
3115  fprintf(stderr,"Biddy_Managed_AddFormula: Unsupported BDD type!\n");
3116  return 0;
3117  }
3118 
3119  return BiddyManagedAddFormula(MNG,x,f,c);
3120 }
3121 
3122 #ifdef __cplusplus
3123 }
3124 #endif
3125 
3126 /***************************************************************************/
3139 #ifdef __cplusplus
3140 extern "C" {
3141 #endif
3142 
3145  unsigned int *idx, Biddy_Edge *f)
3146 {
3147  if (!MNG) MNG = biddyAnonymousManager;
3148 
3149  if (biddyManagerType == BIDDYTYPEOBDD) {
3150  /* IMPLEMENTED */
3151  }
3152  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3153  /* IMPLEMENTED */
3154  }
3155 #ifndef COMPACT
3156  else if (biddyManagerType == BIDDYTYPEZBDD) {
3157  /* IMPLEMENTED */
3158  }
3159  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3160  /* IMPLEMENTED */
3161  }
3162  else if (biddyManagerType == BIDDYTYPETZBDD) {
3163  /* IMPLEMENTED */
3164  }
3165 #endif
3166  else {
3167  fprintf(stderr,"Biddy_Managed_FindFormula: Unsupported BDD type!\n");
3168  return FALSE;
3169  }
3170 
3171  return BiddyManagedFindFormula(MNG,x,idx,f);
3172 }
3173 
3174 #ifdef __cplusplus
3175 }
3176 #endif
3177 
3178 /***************************************************************************/
3192 #ifdef __cplusplus
3193 extern "C" {
3194 #endif
3195 
3198 {
3199  if (!MNG) MNG = biddyAnonymousManager;
3200 
3201  if (biddyManagerType == BIDDYTYPEOBDD) {
3202  /* IMPLEMENTED */
3203  }
3204  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3205  /* IMPLEMENTED */
3206  }
3207 #ifndef COMPACT
3208  else if (biddyManagerType == BIDDYTYPEZBDD) {
3209  /* IMPLEMENTED */
3210  }
3211  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3212  /* IMPLEMENTED */
3213  }
3214  else if (biddyManagerType == BIDDYTYPETZBDD) {
3215  /* IMPLEMENTED */
3216  }
3217 #endif
3218  else {
3219  fprintf(stderr,"Biddy_Managed_DeleteFormula: Unsupported BDD type!\n");
3220  return FALSE;
3221  }
3222 
3223  return BiddyManagedDeleteFormula(MNG,x);
3224 }
3225 
3226 #ifdef __cplusplus
3227 }
3228 #endif
3229 
3230 /***************************************************************************/
3245 #ifdef __cplusplus
3246 extern "C" {
3247 #endif
3248 
3251 {
3252  if (!MNG) MNG = biddyAnonymousManager;
3253 
3254  if (biddyManagerType == BIDDYTYPEOBDD) {
3255  /* IMPLEMENTED */
3256  }
3257  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3258  /* IMPLEMENTED */
3259  }
3260 #ifndef COMPACT
3261  else if (biddyManagerType == BIDDYTYPEZBDD) {
3262  /* IMPLEMENTED */
3263  }
3264  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3265  /* IMPLEMENTED */
3266  }
3267  else if (biddyManagerType == BIDDYTYPETZBDD) {
3268  /* IMPLEMENTED */
3269  }
3270 #endif
3271  else {
3272  fprintf(stderr,"Biddy_Managed_DeleteIthFormula: Unsupported BDD type!\n");
3273  return FALSE;
3274  }
3275 
3276  return BiddyManagedDeleteIthFormula(MNG,i);
3277 }
3278 
3279 #ifdef __cplusplus
3280 }
3281 #endif
3282 
3283 /***************************************************************************/
3295 #ifdef __cplusplus
3296 extern "C" {
3297 #endif
3298 
3299 Biddy_Edge
3301 {
3302  if (!MNG) MNG = biddyAnonymousManager;
3303 
3304  if (biddyManagerType == BIDDYTYPEOBDD) {
3305  /* IMPLEMENTED */
3306  }
3307  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3308  /* IMPLEMENTED */
3309  }
3310 #ifndef COMPACT
3311  else if (biddyManagerType == BIDDYTYPEZBDD) {
3312  /* IMPLEMENTED */
3313  }
3314  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3315  /* IMPLEMENTED */
3316  }
3317  else if (biddyManagerType == BIDDYTYPETZBDD) {
3318  /* IMPLEMENTED */
3319  }
3320 #endif
3321  else {
3322  fprintf(stderr,"Biddy_Managed_GetIthFormula: Unsupported BDD type!\n");
3323  return biddyNull;
3324  }
3325 
3326  return BiddyManagedGetIthFormula(MNG,i);
3327 }
3328 
3329 #ifdef __cplusplus
3330 }
3331 #endif
3332 
3333 /***************************************************************************/
3345 #ifdef __cplusplus
3346 extern "C" {
3347 #endif
3348 
3351 {
3352  if (!MNG) MNG = biddyAnonymousManager;
3353 
3354  if (biddyManagerType == BIDDYTYPEOBDD) {
3355  /* IMPLEMENTED */
3356  }
3357  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3358  /* IMPLEMENTED */
3359  }
3360 #ifndef COMPACT
3361  else if (biddyManagerType == BIDDYTYPEZBDD) {
3362  /* IMPLEMENTED */
3363  }
3364  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3365  /* IMPLEMENTED */
3366  }
3367  else if (biddyManagerType == BIDDYTYPETZBDD) {
3368  /* IMPLEMENTED */
3369  }
3370 #endif
3371  else {
3372  fprintf(stderr,"Biddy_Managed_GetIthFormulaName: Unsupported BDD type!\n");
3373  return NULL;
3374  }
3375 
3376  return BiddyManagedGetIthFormulaName(MNG,i);
3377 }
3378 
3379 #ifdef __cplusplus
3380 }
3381 #endif
3382 
3383 /*******************************************************************************
3384 \brief Function Biddy_Managed_GetOrdering creates a string with a list of
3385  variables ordered according to the active ordering.
3386 
3387 ### Description
3388 ### Side effects
3389  User should free memory for the created string.
3390 ### More info
3391  Macro Biddy_GetOrdering() is defined for use with anonymous manager.
3392 *******************************************************************************/
3393 
3394 #ifdef __cplusplus
3395 extern "C" {
3396 #endif
3397 
3399 Biddy_Managed_GetOrdering(Biddy_Manager MNG)
3400 {
3401  if (!MNG) MNG = biddyAnonymousManager;
3402 
3403  if (biddyManagerType == BIDDYTYPEOBDD) {
3404  /* IMPLEMENTED */
3405  }
3406  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3407  /* IMPLEMENTED */
3408  }
3409 #ifndef COMPACT
3410  else if (biddyManagerType == BIDDYTYPEZBDD) {
3411  /* IMPLEMENTED */
3412  }
3413  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3414  /* IMPLEMENTED */
3415  }
3416  else if (biddyManagerType == BIDDYTYPETZBDD) {
3417  /* IMPLEMENTED */
3418  }
3419 #endif
3420  else {
3421  fprintf(stderr,"Biddy_Managed_GetOrdering: Unsupported BDD type!\n");
3422  return NULL;
3423  }
3424 
3425  return BiddyManagedGetOrdering(MNG);
3426 }
3427 
3428 #ifdef __cplusplus
3429 }
3430 #endif
3431 
3432 /***************************************************************************/
3446 #ifdef __cplusplus
3447 extern "C" {
3448 #endif
3449 
3450 void
3452 {
3453  if (!MNG) MNG = biddyAnonymousManager;
3454 
3455  if (biddyManagerType == BIDDYTYPEOBDD) {
3456  /* IMPLEMENTED */
3457  }
3458  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3459  /* IMPLEMENTED */
3460  }
3461 #ifndef COMPACT
3462  else if (biddyManagerType == BIDDYTYPEZBDD) {
3463  /* IMPLEMENTED */
3464  }
3465  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3466  /* IMPLEMENTED */
3467  }
3468  else if (biddyManagerType == BIDDYTYPETZBDD) {
3469  /* IMPLEMENTED */
3470  }
3471 #endif
3472  else {
3473  fprintf(stderr,"Biddy_Managed_SetOrdering: Unsupported BDD type!\n");
3474  return;
3475  }
3476 
3477  BiddyManagedSetOrdering(MNG,ordering);
3478 }
3479 
3480 #ifdef __cplusplus
3481 }
3482 #endif
3483 
3484 /***************************************************************************/
3498 #ifdef __cplusplus
3499 extern "C" {
3500 #endif
3501 
3502 void
3504 {
3505  if (!MNG) MNG = biddyAnonymousManager;
3506 
3507  if (biddyManagerType == BIDDYTYPEOBDD) {
3508  /* IMPLEMENTED */
3509  }
3510  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3511  /* IMPLEMENTED */
3512  }
3513 #ifndef COMPACT
3514  else if (biddyManagerType == BIDDYTYPEZBDD) {
3515  /* IMPLEMENTED */
3516  }
3517  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3518  /* IMPLEMENTED */
3519  }
3520  else if (biddyManagerType == BIDDYTYPETZBDD) {
3521  /* IMPLEMENTED */
3522  }
3523 #endif
3524  else {
3525  fprintf(stderr,"Biddy_Managed_SetAlphabeticOrdering: Unsupported BDD type!\n");
3526  return;
3527  }
3528 
3529  BiddyManagedSetAlphabeticOrdering(MNG);
3530 }
3531 
3532 #ifdef __cplusplus
3533 }
3534 #endif
3535 
3536 /***************************************************************************/
3550 #ifdef __cplusplus
3551 extern "C" {
3552 #endif
3553 
3556 {
3557  if (!MNG) MNG = biddyAnonymousManager;
3558 
3559  if (biddyManagerType == BIDDYTYPEOBDD) {
3560  /* IMPLEMENTED */
3561  }
3562  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3563  /* IMPLEMENTED */
3564  }
3565 #ifndef COMPACT
3566  else if (biddyManagerType == BIDDYTYPEZBDD) {
3567  /* IMPLEMENTED */
3568  }
3569  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3570  /* IMPLEMENTED */
3571  }
3572  else if (biddyManagerType == BIDDYTYPETZBDD) {
3573  /* IMPLEMENTED */
3574  }
3575 #endif
3576  else {
3577  fprintf(stderr,"Biddy_Managed_SwapWithHigher: Unsupported BDD type!\n");
3578  return 0;
3579  }
3580 
3581  return BiddyManagedSwapWithHigher(MNG,v);
3582 }
3583 
3584 #ifdef __cplusplus
3585 }
3586 #endif
3587 
3588 /***************************************************************************/
3602 #ifdef __cplusplus
3603 extern "C" {
3604 #endif
3605 
3608 {
3609  if (!MNG) MNG = biddyAnonymousManager;
3610 
3611  if (biddyManagerType == BIDDYTYPEOBDD) {
3612  /* IMPLEMENTED */
3613  }
3614  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3615  /* IMPLEMENTED */
3616  }
3617 #ifndef COMPACT
3618  else if (biddyManagerType == BIDDYTYPEZBDD) {
3619  /* IMPLEMENTED */
3620  }
3621  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3622  /* IMPLEMENTED */
3623  }
3624  else if (biddyManagerType == BIDDYTYPETZBDD) {
3625  /* IMPLEMENTED */
3626  }
3627 #endif
3628  else {
3629  fprintf(stderr,"Biddy_Managed_SwapWithLower: Unsupported BDD type!\n");
3630  return 0;
3631  }
3632 
3633  return BiddyManagedSwapWithLower(MNG,v);
3634 }
3635 
3636 #ifdef __cplusplus
3637 }
3638 #endif
3639 
3640 /***************************************************************************/
3658 #ifdef __cplusplus
3659 extern "C" {
3660 #endif
3661 
3664 {
3665  if (!MNG) MNG = biddyAnonymousManager;
3666  ZF_LOGI("Biddy_Sifting");
3667 
3668  if (biddyManagerType == BIDDYTYPEOBDD) {
3669  /* IMPLEMENTED */
3670  }
3671  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3672  /* IMPLEMENTED */
3673  }
3674 #ifndef COMPACT
3675  else if (biddyManagerType == BIDDYTYPEZBDD) {
3676  /* IMPLEMENTED */
3677  }
3678  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3679  /* IMPLEMENTED */
3680  }
3681  else if (biddyManagerType == BIDDYTYPETZBDD) {
3682  /* IMPLEMENTED */
3683  }
3684 #endif
3685  else {
3686  fprintf(stderr,"Biddy_Managed_Sifting: Unsupported BDD type!\n");
3687  return FALSE;
3688  }
3689 
3690  return BiddyManagedSifting(MNG,f,converge);
3691 }
3692 
3693 #ifdef __cplusplus
3694 }
3695 #endif
3696 
3697 /***************************************************************************/
3718 #ifdef __cplusplus
3719 extern "C" {
3720 #endif
3721 
3722 void
3724 {
3725  if (!MNG) MNG = biddyAnonymousManager;
3726 
3727  if (biddyManagerType == BIDDYTYPEOBDD) {
3728  /* IMPLEMENTED */
3729  }
3730  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3731  /* IMPLEMENTED */
3732  }
3733 #ifndef COMPACT
3734  else if (biddyManagerType == BIDDYTYPEZBDD) {
3735  /* IMPLEMENTED */
3736  }
3737  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3738  /* IMPLEMENTED */
3739  }
3740  else if (biddyManagerType == BIDDYTYPETZBDD) {
3741  /* IMPLEMENTED */
3742  }
3743 #endif
3744  else {
3745  fprintf(stderr,"Biddy_Managed_MinimizeBDD: Unsupported BDD type!\n");
3746  return;
3747  }
3748 
3749  BiddyManagedMinimizeBDD(MNG,name);
3750 }
3751 
3752 #ifdef __cplusplus
3753 }
3754 #endif
3755 
3756 /***************************************************************************/
3777 #ifdef __cplusplus
3778 extern "C" {
3779 #endif
3780 
3781 void
3783 {
3784  if (!MNG) MNG = biddyAnonymousManager;
3785 
3786  if (biddyManagerType == BIDDYTYPEOBDD) {
3787  /* IMPLEMENTED */
3788  }
3789  else if (biddyManagerType == BIDDYTYPEOBDDC) {
3790  /* IMPLEMENTED */
3791  }
3792 #ifndef COMPACT
3793  else if (biddyManagerType == BIDDYTYPEZBDD) {
3794  /* IMPLEMENTED */
3795  }
3796  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3797  /* IMPLEMENTED */
3798  }
3799  else if (biddyManagerType == BIDDYTYPETZBDD) {
3800  /* IMPLEMENTED */
3801  }
3802 #endif
3803  else {
3804  fprintf(stderr,"Biddy_Managed_MaximizeBDD: Unsupported BDD type!\n");
3805  return;
3806  }
3807 
3808  BiddyManagedMaximizeBDD(MNG,name);
3809 }
3810 
3811 #ifdef __cplusplus
3812 }
3813 #endif
3814 
3815 /***************************************************************************/
3839 #ifdef __cplusplus
3840 extern "C" {
3841 #endif
3842 
3843 Biddy_Edge
3845 {
3846  if (!MNG1) MNG1 = biddyAnonymousManager;
3847  ZF_LOGI("Biddy_Copy");
3848 
3849  if (biddyManagerType1 == BIDDYTYPEOBDD) {
3850  /* IMPLEMENTED */
3851  }
3852  else if (biddyManagerType1 == BIDDYTYPEOBDDC) {
3853  /* IMPLEMENTED */
3854  }
3855 #ifndef COMPACT
3856  else if (biddyManagerType1 == BIDDYTYPEZBDD) {
3857  /* IMPLEMENTED */
3858  }
3859  else if (biddyManagerType1 == BIDDYTYPEZBDDC) {
3860  /* IMPLEMENTED */
3861  }
3862  else if (biddyManagerType1 == BIDDYTYPETZBDD) {
3863  /* IMPLEMENTED */
3864  }
3865 #endif
3866  else {
3867  fprintf(stderr,"Biddy_Managed_Copy: Unsupported BDD type!\n");
3868  return biddyNull;
3869  }
3870 
3871  if (biddyManagerType2 == BIDDYTYPEOBDD) {
3872  /* IMPLEMENTED */
3873  }
3874  else if (biddyManagerType2 == BIDDYTYPEOBDDC) {
3875  /* IMPLEMENTED */
3876  }
3877 #ifndef COMPACT
3878  else if (biddyManagerType2 == BIDDYTYPEZBDD) {
3879  /* IMPLEMENTED */
3880  }
3881  else if (biddyManagerType2 == BIDDYTYPEZBDDC) {
3882  /* IMPLEMENTED */
3883  }
3884  else if (biddyManagerType2 == BIDDYTYPETZBDD) {
3885  /* IMPLEMENTED */
3886  }
3887 #endif
3888  else {
3889  fprintf(stderr,"Biddy_Managed_Copy: Unsupported BDD type!\n");
3890  return biddyNull;
3891  }
3892 
3893  return BiddyManagedCopy(MNG1,MNG2,f,TRUE);
3894 }
3895 
3896 #ifdef __cplusplus
3897 }
3898 #endif
3899 
3900 /***************************************************************************/
3916 #ifdef __cplusplus
3917 extern "C" {
3918 #endif
3919 
3920 void
3922 {
3923  if (!MNG1) MNG1 = biddyAnonymousManager;
3924 
3925  if (biddyManagerType1 == BIDDYTYPEOBDD) {
3926  /* IMPLEMENTED */
3927  }
3928  else if (biddyManagerType1 == BIDDYTYPEOBDDC) {
3929  /* IMPLEMENTED */
3930  }
3931 #ifndef COMPACT
3932  else if (biddyManagerType1 == BIDDYTYPEZBDD) {
3933  /* IMPLEMENTED */
3934  }
3935  else if (biddyManagerType1 == BIDDYTYPEZBDDC) {
3936  /* IMPLEMENTED */
3937  }
3938  else if (biddyManagerType1 == BIDDYTYPETZBDD) {
3939  /* IMPLEMENTED */
3940  }
3941 #endif
3942  else {
3943  fprintf(stderr,"Biddy_Managed_CopyFormula: Unsupported BDD type!\n");
3944  return;
3945  }
3946 
3947  if (biddyManagerType2 == BIDDYTYPEOBDD) {
3948  /* IMPLEMENTED */
3949  }
3950  else if (biddyManagerType2 == BIDDYTYPEOBDDC) {
3951  /* IMPLEMENTED */
3952  }
3953 #ifndef COMPACT
3954  else if (biddyManagerType2 == BIDDYTYPEZBDD) {
3955  /* IMPLEMENTED */
3956  }
3957  else if (biddyManagerType2 == BIDDYTYPEZBDDC) {
3958  /* IMPLEMENTED */
3959  }
3960  else if (biddyManagerType2 == BIDDYTYPETZBDD) {
3961  /* IMPLEMENTED */
3962  }
3963 #endif
3964  else {
3965  fprintf(stderr,"Biddy_Managed_CopyFormula: Unsupported BDD type!\n");
3966  return;
3967  }
3968 
3969  BiddyManagedCopyFormula(MNG1,MNG2,x);
3970 }
3971 
3972 #ifdef __cplusplus
3973 }
3974 #endif
3975 
3976 /***************************************************************************/
4011 #ifdef __cplusplus
4012 extern "C" {
4013 #endif
4014 
4015 Biddy_Edge
4016 Biddy_Managed_ConstructBDD(Biddy_Manager MNG, int numV, Biddy_String varlist, int numN,
4017  Biddy_String nodelist)
4018 {
4019  if (!MNG) MNG = biddyAnonymousManager;
4020 
4021  if (biddyManagerType == BIDDYTYPEOBDD) {
4022  /* IMPLEMENTED */
4023  }
4024  else if (biddyManagerType == BIDDYTYPEOBDDC) {
4025  /* IMPLEMENTED */
4026  }
4027 #ifndef COMPACT
4028  else if (biddyManagerType == BIDDYTYPEZBDD) {
4029  /* IMPLEMENTED */
4030  }
4031  else if (biddyManagerType == BIDDYTYPEZBDDC) {
4032  /* IMPLEMENTED */
4033  }
4034  else if (biddyManagerType == BIDDYTYPETZBDD) {
4035  /* IMPLEMENTED */
4036  }
4037 #endif
4038  else {
4039  fprintf(stderr,"Biddy_Managed_ConstructBDD: Unsupported BDD type!\n");
4040  return biddyNull;
4041  }
4042 
4043  return BiddyManagedConstructBDD(MNG,numV,varlist,numN,nodelist);
4044 }
4045 
4046 #ifdef __cplusplus
4047 }
4048 #endif
4049 
4050 /*----------------------------------------------------------------------------*/
4051 /* Definition of internal functions used to implement external functions */
4052 /*----------------------------------------------------------------------------*/
4053 
4054 /***************************************************************************/
4063 void
4064 BiddyInitMNG(Biddy_Manager *mng, int bddtype)
4065 {
4066  Biddy_Manager MNG;
4067  unsigned int i;
4068 #ifdef VARIABLEORDERINGMATRIX_YES
4069  unsigned int j;
4070 #endif
4071 
4072 #ifdef UNIX
4073  struct timeval tv;
4074  struct rlimit rl;
4075 #endif
4076 
4077 #ifdef PLAIN
4078  if ((bddtype == BIDDYTYPETZBDDC) || (bddtype == BIDDYTYPETZBDD) ||
4079  (bddtype == BIDDYTYPETZFDDC) || (bddtype == BIDDYTYPETZFDD))
4080  {
4081  fprintf(stderr,"This instance of Biddy library was compiled with -DPLAIN.\n");
4082  fprintf(stderr,"Tagged binary decision diagrams are not supported.\n");
4083  exit(1);
4084  }
4085 #endif
4086 
4087 #ifdef UNIX
4088  /* printf("The page size for this system is %ld bytes.\n", sysconf(_SC_PAGESIZE)); */
4089  rl.rlim_max = rl.rlim_cur = RLIM_INFINITY;
4090  if (setrlimit(RLIMIT_STACK, &rl)) {
4091  fprintf(stderr,"ERROR: setrlimit\n");
4092  perror("setrlimit");
4093  exit(1);
4094  }
4095 #endif
4096 
4097 #ifdef UNIXXX
4098  mallopt(M_MMAP_MAX,0);
4099  mallopt(M_TRIM_THRESHOLD,-1);
4100 #endif
4101 
4102  /* RANDOM NUMBERS GENERATOR */
4103 #ifdef UNIX
4104  gettimeofday(&tv,0);
4105  srand(tv.tv_usec);
4106 #else
4107  srand((unsigned int) time(NULL));
4108 #endif
4109 
4110  if (!mng) {
4111  if (!(biddyAnonymousManager = (Biddy_Manager) malloc(sizeof(BiddyManager)))) {
4112  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4113  exit(1);
4114  }
4115  MNG = biddyAnonymousManager;
4116  } else {
4117  if (!(*mng = (Biddy_Manager) malloc(sizeof(BiddyManager)))) {
4118  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4119  exit(1);
4120  }
4121  MNG = *mng;
4122  }
4123 
4124  /* DEBUGGING */
4125  /*
4126  printf("DEBUG (BiddyInitMNG): BiddyInitMNG STARTED\n");
4127  printf("DEBUG (BiddyInitMNG): mng = %p\n",mng);
4128  printf("DEBUG (BiddyInitMNG): bddtype = %d\n",bddtype);
4129  printf("DEBUG (BiddyInitMNG): MNG = %p\n",MNG);
4130  */
4131 
4132  /* CREATION OF MANAGER'S STRUCTURES - VALUES ARE NOT INITIALIZED HERE */
4133  MNG[0] = NULL; /* biddyManagerName */
4134  if (!(MNG[1] = (short int *) malloc(sizeof(short int)))) {
4135  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4136  exit(1);
4137  }
4138  biddyManagerType = 0;
4139  MNG[2] = NULL; /* biddyTerminal */
4140  MNG[3] = NULL; /* biddyZero */
4141  MNG[4] = NULL; /* biddyOne */
4142  if (!(MNG[5] = (BiddyNodeTable *) malloc(sizeof(BiddyNodeTable)))) {
4143  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4144  exit(1);
4145  }
4146  biddyNodeTable.table = NULL;
4147  biddyNodeTable.blocktable = NULL;
4148  biddyNodeTable.initsize = 0;
4149  biddyNodeTable.size = 0;
4150  biddyNodeTable.limitsize = 0;
4151  biddyNodeTable.blocknumber = 0;
4152  biddyNodeTable.initblocksize = 0;
4153  biddyNodeTable.blocksize = 0;
4154  biddyNodeTable.limitblocksize = 0;
4155  biddyNodeTable.generated = 0;
4156  biddyNodeTable.max = 0;
4157  biddyNodeTable.num = 0;
4158  biddyNodeTable.garbage = 0;
4159  biddyNodeTable.swap = 0;
4160  biddyNodeTable.sifting = 0;
4161  biddyNodeTable.nodetableresize = 0;
4162  biddyNodeTable.funite = 0;
4163  biddyNodeTable.funandor = 0;
4164  biddyNodeTable.funxor = 0;
4165  biddyNodeTable.gctime = 0;
4166  biddyNodeTable.drtime = 0;
4167  biddyNodeTable.gcratio = 0.0;
4168  biddyNodeTable.gcratioF = 0.0;
4169  biddyNodeTable.gcratioX = 0.0;
4170  biddyNodeTable.resizeratio = 0.0;
4171  biddyNodeTable.resizeratioF = 0.0;
4172  biddyNodeTable.resizeratioX = 0.0;
4173  biddyNodeTable.siftingtreshold = 0.0;
4174  biddyNodeTable.convergesiftingtreshold = 0.0;
4175 #ifdef BIDDYEXTENDEDSTATS_YES
4176  biddyNodeTable.foa = 0;
4177  biddyNodeTable.find = 0;
4178  biddyNodeTable.compare = 0;
4179  biddyNodeTable.add = 0;
4180  biddyNodeTable.iterecursive = 0;
4181  biddyNodeTable.andorrecursive = 0;
4182  biddyNodeTable.xorrecursive = 0;
4183  biddyNodeTable.gcobsolete = NULL;
4184 #endif
4185  if (!(MNG[6] = (BiddyVariableTable *) malloc(sizeof(BiddyVariableTable)))) {
4186  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4187  exit(1);
4188  }
4189  biddyVariableTable.table = NULL;
4190  biddyVariableTable.lookup = NULL;
4191  biddyVariableTable.size = 0;
4192  biddyVariableTable.num = 0;
4193  biddyVariableTable.numnum = 0;
4194  if (!(MNG[7] = (BiddyFormulaTable *) malloc(sizeof(BiddyFormulaTable)))) {
4195  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4196  exit(1);
4197  }
4198  biddyFormulaTable.table = NULL;
4199  biddyFormulaTable.size = 0;
4200  biddyFormulaTable.numOrdered = 0;
4201  biddyFormulaTable.deletedName = NULL;
4202  if (!(MNG[8] = (BiddyOp3CacheTable *) malloc(sizeof(BiddyOp3CacheTable)))) {
4203  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4204  exit(1);
4205  }
4206  biddyOPCache.table = NULL;
4207  biddyOPCache.size = 0;
4208  biddyOPCache.disabled = FALSE;
4209  if (!(biddyOPCache.notusedyet = (Biddy_Boolean *) malloc(sizeof(Biddy_Boolean)))) {
4210  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4211  exit(1);
4212  }
4213  *(biddyOPCache.notusedyet) = FALSE;
4214 #ifdef BIDDYEXTENDEDSTATS_YES
4215  if (!(biddyOPCache.search = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4216  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4217  exit(1);
4218  }
4219  if (!(biddyOPCache.find = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4220  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4221  exit(1);
4222  }
4223  if (!(biddyOPCache.insert = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4224  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4225  exit(1);
4226  }
4227  if (!(biddyOPCache.overwrite = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4228  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4229  exit(1);
4230  }
4231  *(biddyOPCache.search) = 0;
4232  *(biddyOPCache.find) = 0;
4233  *(biddyOPCache.insert) = 0;
4234  *(biddyOPCache.overwrite) = 0;
4235 #endif
4236  if (!(MNG[9] = (BiddyOp3CacheTable *) malloc(sizeof(BiddyOp3CacheTable)))) {
4237  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4238  exit(1);
4239  }
4240  biddyEACache.table = NULL;
4241  biddyEACache.size = 0;
4242  biddyEACache.disabled = FALSE;
4243  if (!(biddyEACache.notusedyet = (Biddy_Boolean *) malloc(sizeof(Biddy_Boolean)))) {
4244  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4245  exit(1);
4246  }
4247  *(biddyEACache.notusedyet) = FALSE;
4248 #ifdef BIDDYEXTENDEDSTATS_YES
4249  if (!(biddyEACache.search = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4250  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4251  exit(1);
4252  }
4253  if (!(biddyEACache.find = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4254  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4255  exit(1);
4256  }
4257  if (!(biddyEACache.insert = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4258  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4259  exit(1);
4260  }
4261  if (!(biddyEACache.overwrite = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4262  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4263  exit(1);
4264  }
4265  *(biddyEACache.search) = 0;
4266  *(biddyEACache.find) = 0;
4267  *(biddyEACache.insert) = 0;
4268  *(biddyEACache.overwrite) = 0;
4269 #endif
4270  if (!(MNG[10] = (BiddyOp3CacheTable *) malloc(sizeof(BiddyOp3CacheTable)))) {
4271  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4272  exit(1);
4273  }
4274  biddyRCCache.table = NULL;
4275  biddyRCCache.size = 0;
4276  biddyRCCache.disabled = FALSE;
4277  if (!(biddyRCCache.notusedyet = (Biddy_Boolean *) malloc(sizeof(Biddy_Boolean)))) {
4278  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4279  exit(1);
4280  }
4281  *(biddyRCCache.notusedyet) = FALSE;
4282 #ifdef BIDDYEXTENDEDSTATS_YES
4283  if (!(biddyRCCache.search = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4284  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4285  exit(1);
4286  }
4287  if (!(biddyRCCache.find = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4288  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4289  exit(1);
4290  }
4291  if (!(biddyRCCache.insert = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4292  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4293  exit(1);
4294  }
4295  if (!(biddyRCCache.overwrite = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4296  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4297  exit(1);
4298  }
4299  *(biddyRCCache.search) = 0;
4300  *(biddyRCCache.find) = 0;
4301  *(biddyRCCache.insert) = 0;
4302  *(biddyRCCache.overwrite) = 0;
4303 #endif
4304  if (!(MNG[11] = (BiddyKeywordCacheTable *) malloc(sizeof(BiddyKeywordCacheTable)))) {
4305  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4306  exit(1);
4307  }
4308  biddyReplaceCache.table = NULL;
4309  biddyReplaceCache.size = 0;
4310  biddyReplaceCache.keywordList = NULL;
4311  biddyReplaceCache.keyList = NULL;
4312  biddyReplaceCache.keyNum = 0;
4313  biddyReplaceCache.keywordNum = 0;
4314  biddyReplaceCache.disabled = FALSE;
4315  if (!(biddyReplaceCache.notusedyet = (Biddy_Boolean *) malloc(sizeof(Biddy_Boolean)))) {
4316  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4317  exit(1);
4318  }
4319  *(biddyReplaceCache.notusedyet) = FALSE;
4320 #ifdef BIDDYEXTENDEDSTATS_YES
4321  if (!(biddyReplaceCache.search = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4322  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4323  exit(1);
4324  }
4325  if (!(biddyReplaceCache.find = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4326  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4327  exit(1);
4328  }
4329  if (!(biddyReplaceCache.insert = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4330  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4331  exit(1);
4332  }
4333  if (!(biddyReplaceCache.overwrite = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
4334  fprintf(stderr, "BiddyInitMNG: Out of memoy!\n");
4335  exit(1);
4336  }
4337  *(biddyReplaceCache.search) = 0;
4338  *(biddyReplaceCache.find) = 0;
4339  *(biddyReplaceCache.insert) = 0;
4340  *(biddyReplaceCache.overwrite) = 0;
4341 #endif
4342  if (!(MNG[12] = (BiddyCacheList* *) malloc(sizeof(BiddyCacheList*)))) {
4343  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4344  exit(1);
4345  }
4346  biddyCacheList = NULL;
4347  if (!(MNG[13] = (BiddyNode* *) malloc(sizeof(BiddyNode*)))) {
4348  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4349  exit(1);
4350  }
4351  biddyFreeNodes = NULL;
4352  if (!(MNG[14] = (BiddyOrderingTable *) malloc(sizeof(BiddyOrderingTable)))) {
4353  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4354  exit(1);
4355  }
4356  if (!(MNG[15] = (unsigned int *) malloc(sizeof(unsigned int)))) {
4357  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4358  exit(1);
4359  }
4360  biddySystemAge = 0;
4361  if (!(MNG[16] = (unsigned short int *) malloc(sizeof(unsigned short int)))) {
4362  fprintf(stderr,"BiddyInitMNG: Out of memoy!\n");
4363  exit(1);
4364  }
4365  biddySelect = 0;
4366 
4367  /* INITIALIZATION OF MANAGER'S STRUCTURES - VALUES ARE NOW INITIALIZED */
4368  if (bddtype == BIDDYTYPEOBDD) {
4369  MNG[0] = strdup(BIDDYTYPENAMEOBDD); /* biddyManagerName */
4370  } else if (bddtype == BIDDYTYPEOBDDC) {
4371  MNG[0] = strdup(BIDDYTYPENAMEOBDDC); /* biddyManagerName */
4372  }
4373 #ifndef COMPACT
4374  else if (bddtype == BIDDYTYPEZBDD) {
4375  MNG[0] = strdup(BIDDYTYPENAMEZBDD); /* biddyManagerName */
4376  } else if (bddtype == BIDDYTYPEZBDDC) {
4377  MNG[0] = strdup(BIDDYTYPENAMEZBDDC); /* biddyManagerName */
4378  } else if (bddtype == BIDDYTYPETZBDD) {
4379 #if UINTPTR_MAX == 0xffffffffffffffff
4380 #else
4381  fprintf(stderr,"BiddyInitMNG: TZBDDs are supported on 64-bit architecture, only!\n");
4382  exit(1);
4383 #endif
4384  MNG[0] = strdup(BIDDYTYPENAMETZBDD); /* biddyManagerName */
4385  } else if (bddtype == BIDDYTYPETZBDDC) {
4386 #if UINTPTR_MAX == 0xffffffffffffffff
4387 #else
4388  fprintf(stderr,"BiddyInitMNG: TZBDDs are supported on 64-bit architecture, only!\n");
4389  exit(1);
4390 #endif
4391  MNG[0] = strdup(BIDDYTYPENAMETZBDDC); /* biddyManagerName */
4392  fprintf(stderr,"BiddyInitMNG: %s is not supported, yet!\n",BIDDYTYPENAMETZBDDC);
4393  exit(1);
4394  } else if (bddtype == BIDDYTYPEOFDD) {
4395  MNG[0] = strdup(BIDDYTYPENAMEOFDD); /* biddyManagerName */
4396  fprintf(stderr,"BiddyInitMNG: %s is not supported, yet!\n",BIDDYTYPENAMEOFDD);
4397  exit(1);
4398  } else if (bddtype == BIDDYTYPEOFDDC) {
4399  MNG[0] = strdup(BIDDYTYPENAMEOFDDC); /* biddyManagerName */
4400  fprintf(stderr,"BiddyInitMNG: %s is not supported, yet!\n",BIDDYTYPENAMEOFDDC);
4401  exit(1);
4402  } else if (bddtype == BIDDYTYPEZFDD) {
4403  MNG[0] = strdup(BIDDYTYPENAMEZFDD); /* biddyManagerName */
4404  fprintf(stderr,"BiddyInitMNG: %s is not supported, yet!\n",BIDDYTYPENAMEZFDD);
4405  exit(1);
4406  } else if (bddtype == BIDDYTYPEZFDDC) {
4407  MNG[0] = strdup(BIDDYTYPENAMEZFDDC); /* biddyManagerName */
4408  fprintf(stderr,"BiddyInitMNG: %s is not supported, yet!\n",BIDDYTYPENAMEZFDDC);
4409  exit(1);
4410  } else if (bddtype == BIDDYTYPETZFDD) {
4411 #if UINTPTR_MAX == 0xffffffffffffffff
4412 #else
4413  fprintf(stderr,"BiddyInitMNG: TZFDDs are supported on 64-bit architecture, only!\n");
4414  exit(1);
4415 #endif
4416  MNG[0] = strdup(BIDDYTYPENAMETZFDD); /* biddyManagerName */
4417  fprintf(stderr,"BiddyInitMNG: %s is not supported, yet!\n",BIDDYTYPENAMETZFDD);
4418  exit(1);
4419  } else if (bddtype == BIDDYTYPETZFDDC) {
4420 #if UINTPTR_MAX == 0xffffffffffffffff
4421 #else
4422  fprintf(stderr,"BiddyInitMNG: TZFDDs are supported on 64-bit architecture, only!\n");
4423  exit(1);
4424 #endif
4425  MNG[0] = strdup(BIDDYTYPENAMETZFDDC); /* biddyManagerName */
4426  fprintf(stderr,"BiddyInitMNG: %s is not supported, yet!\n",BIDDYTYPENAMETZFDDC);
4427  exit(1);
4428  } else {
4429  fprintf(stderr,"BiddyInitMNG: Unsupported BDD type!\n");
4430  exit(1);
4431  }
4432 #else
4433  else {
4434  fprintf(stderr,"BiddyInitMNG: This variant of Biddy library supports ROBDD, only!\n");
4435  exit(1);
4436  }
4437 #endif
4438 
4439  /* THESE ARE MAIN SETTINGS FOR MEMORY MANAGEMENT AND GC */
4440  biddyManagerType = bddtype;
4441  biddyVariableTable.size = BIDDYVARIABLETABLESIZE;
4442  biddyNodeTable.initblocksize = BIDDYNODETABLEINITBLOCKSIZE;
4443  biddyNodeTable.limitblocksize = BIDDYNODETABLELIMITBLOCKSIZE;
4444  biddyNodeTable.initsize = BIDDYNODETABLEINITSIZE;
4445  biddyNodeTable.limitsize = BIDDYNODETABLELIMITSIZE;
4446  biddyOPCache.size = BIDDYOPCACHESIZE;
4447  biddyEACache.size = BIDDYEACACHESIZE;
4448  biddyRCCache.size = BIDDYRCCACHESIZE;
4449  biddyReplaceCache.size = BIDDYREPLACECACHESIZE;
4450  biddyNodeTable.gcratio = (float) BIDDYNODETABLEGCRATIO; /* do not delete nodes if the effect is to small, gcratio */
4451  biddyNodeTable.gcratioF = (float) BIDDYNODETABLEGCRATIOF; /* do not delete nodes if the effect is to small, gcratio */
4452  biddyNodeTable.gcratioX = (float) BIDDYNODETABLEGCRATIOX; /* do not delete nodes if the effect is to small, gcratio */
4453  biddyNodeTable.resizeratio = (float) BIDDYNODETABLERESIZERATIO; /* resize Node table if there are to many nodes */
4454  biddyNodeTable.resizeratioF = (float) BIDDYNODETABLERESIZERATIOF; /* resize Node table if there are to many nodes */
4455  biddyNodeTable.resizeratioX = (float) BIDDYNODETABLERESIZERATIOX; /* resize Node table if there are to many nodes */
4456  biddyNodeTable.siftingtreshold = (float) BIDDYNODETABLESIFTINGTRESHOLD; /* stop sifting if the size of the system grows to much */
4457  biddyNodeTable.convergesiftingtreshold = (float) BIDDYNODETABLECONVERGESIFTINGTRESHOLD; /* stop one step of converging sifting if the size of the system grows to much */
4458  biddyNodeTable.siftingfactor = (float) BIDDYNODETABLESIFTINGFACTOR; /* sifting heuristics */
4459 
4460  /* CREATE AND INITIALIZE NODE TABLE */
4461  /* THE ACTUAL SIZE OF NODE TABLE IS biddyNodeTable.size+2 */
4462  /* BECAUSE OF USED TRICKS, HASH FUNCTION MUST NEVER RETURN ZERO! */
4463  /* USEFUL INDICES ARE FROM [1] TO [biddyNodeTable.size+1] */
4464  biddyNodeTable.size = biddyNodeTable.initsize;
4465  if (!(biddyNodeTable.table = (BiddyNode **)
4466  calloc((biddyNodeTable.size+2),sizeof(BiddyNode *)))) {
4467  fprintf(stderr,"BiddyInitMNG (node table): Out of memoy!\n");
4468  exit(1);
4469  }
4470  /* for (i=0;i<=biddyNodeTable.size+1;i++) biddyNodeTable.table[i] = NULL; */
4471 
4472  /* CREATE AND INITIALIZE VARIABLE TABLE */
4473  /* VARIABLE "1" HAS INDEX = 0 and global order = size-1 */
4474  /* VARIABLES ARE ORDERED BY INDEX IN THE VARIABLE TABLE */
4475  /* IN THE BDD, SMALLER (PREV) VARIABLES ARE ABOVE THE GREATER (NEXT) ONES */
4476  /* VARIABLE "1" MUST ALWAYS HAVE MAX GLOBAL ORDER (IT IS BOTTOMMOST) */
4477  /* THIS PART OF CODE DETERMINES DEFAULT ORDERING FOR NEW VARIABLES: */
4478  /* ORDER FOR OBDDs AND OFDDs: [1] < [2] < ... < [size-1] < [0] */
4479  /* ORDER FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: [size-1] < [size-2] < ... < [1] < [0] */
4480  /* FOR OBDDs AND OFDDs: the topmost variable always has prev=biddyVariableTable.size */
4481  /* FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: the topmost variable always has prev=biddyVariableTable.num */
4482  biddyVariableTable.table = (BiddyVariable *)
4483  malloc(biddyVariableTable.size * sizeof(BiddyVariable));
4484  biddyVariableTable.table[0].name = strdup("1");
4485  biddyVariableTable.table[0].num = 1;
4486  biddyVariableTable.table[0].firstNode = NULL;
4487  biddyVariableTable.table[0].lastNode = NULL;
4488  biddyVariableTable.table[0].variable = biddyNull;
4489  biddyVariableTable.table[0].element = biddyNull;
4490  biddyVariableTable.table[0].selected = FALSE;
4491  biddyVariableTable.table[0].data = NULL;
4492  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD))
4493  {
4494  biddyVariableTable.table[0].prev = biddyVariableTable.size;
4495  biddyVariableTable.table[0].next = 0; /* fixed */
4496  }
4497 #ifndef COMPACT
4498  else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
4499  {
4500  biddyVariableTable.table[0].prev = biddyVariableTable.size;
4501  biddyVariableTable.table[0].next = 0; /* fixed */
4502  }
4503  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
4504  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
4505  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
4506  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
4507  {
4508  biddyVariableTable.table[0].prev = 1;
4509  biddyVariableTable.table[0].next = 0; /* fixed */
4510  }
4511 #endif
4512  nullOrdering(biddyOrderingTable);
4513 #ifndef VARIABLEORDERINGMATRIX_YES
4514  biddyOrderingTable[0] = biddyVariableTable.size-1;
4515 #endif
4516  for (i=1; i<biddyVariableTable.size; i++) {
4517  biddyVariableTable.table[i].name = NULL;
4518  biddyVariableTable.table[i].num = 0;
4519  biddyVariableTable.table[i].firstNode = NULL;
4520  biddyVariableTable.table[i].lastNode = NULL;
4521  biddyVariableTable.table[i].variable = biddyNull;
4522  biddyVariableTable.table[i].element = biddyNull;
4523  biddyVariableTable.table[i].selected = FALSE;
4524  biddyVariableTable.table[i].data = NULL;
4525 #ifdef VARIABLEORDERINGMATRIX_YES
4526  SET_ORDER(biddyOrderingTable,i,0);
4527 #endif
4528  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD))
4529  {
4530  biddyVariableTable.table[i].prev = i-1;
4531  biddyVariableTable.table[i].next = i+1;
4532 #ifdef VARIABLEORDERINGMATRIX_YES
4533  for (j=i+1; j<biddyVariableTable.size; j++) {
4534  SET_ORDER(biddyOrderingTable,i,j);
4535  }
4536 #else
4537  biddyOrderingTable[i] = i-1;
4538 #endif
4539  }
4540 #ifndef COMPACT
4541  else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
4542  {
4543  biddyVariableTable.table[i].prev = i-1;
4544  biddyVariableTable.table[i].next = i+1;
4545 #ifdef VARIABLEORDERINGMATRIX_YES
4546  for (j=i+1; j<biddyVariableTable.size; j++) {
4547  SET_ORDER(biddyOrderingTable,i,j);
4548  }
4549 #else
4550  biddyOrderingTable[i] = i-1;
4551 #endif
4552  }
4553  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
4554  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
4555  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
4556  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
4557  {
4558  biddyVariableTable.table[i].prev = i+1;
4559  biddyVariableTable.table[i].next = i-1;
4560 #ifdef VARIABLEORDERINGMATRIX_YES
4561  for (j=1; j<i; j++) {
4562  SET_ORDER(biddyOrderingTable,i,j);
4563  }
4564 #else
4565  biddyOrderingTable[i] = biddyVariableTable.size-i-1;
4566 #endif
4567  }
4568 #endif
4569  }
4570  biddyVariableTable.num = 1; /* ONLY VARIABLE '1' IS CREATED */
4571  biddyVariableTable.numnum = 1; /* VARIABLE '1' IS A NUMBERED VARIABLE */
4572 
4573  /* LOOKUP TABLE FOR FASTER SEARCHING OF VARIABLES */
4574  /* THIS IS NOT FULLY IMPLEMENTED AND NOT USED, YET */
4575  biddyVariableTable.lookup = (BiddyLookupVariable *)
4576  malloc(biddyVariableTable.size * sizeof(BiddyLookupVariable));
4577  biddyVariableTable.lookup[0].name = strdup("1");
4578  biddyVariableTable.lookup[0].v = 0;
4579 
4580  /* DEBUGGING */
4581  /*
4582  writeORDER(MNG);
4583  */
4584 
4585  /* DEBUGGING */
4586  /*
4587  warshall(biddyOrderingTable,BiddyManagedVariableTableNum(MNG));
4588  writeORDER(MNG);
4589  */
4590 
4591  /* INITIALIZATION OF MEMORY MANAGEMENT */
4592  /* ALLOCATE FIRST CHUNK OF NODES */
4593  biddyNodeTable.blocksize = biddyNodeTable.initblocksize;
4594  if (!(biddyFreeNodes = (BiddyNode *)
4595  malloc((biddyNodeTable.blocksize) * sizeof(BiddyNode)))) {
4596  fprintf(stderr,"BiddyInitMNG (nodes): Out of memoy!\n");
4597  exit(1);
4598  }
4599  if (!(biddyNodeTable.blocktable = (BiddyNode **)malloc(sizeof(BiddyNode *)))) {
4600  fprintf(stderr, "BiddyInitMNG (blocktable): Out of memoy!\n");
4601  exit(1);
4602  }
4603  biddyNodeTable.blocktable[0] = biddyFreeNodes;
4604  biddyNodeTable.table[0] = biddyFreeNodes;
4605  biddyFreeNodes = &biddyFreeNodes[1];
4606  for (i=0; i<biddyNodeTable.blocksize-2; i++) {
4607  biddyFreeNodes[i].list = (void *) &biddyFreeNodes[i+1];
4608  }
4609  biddyFreeNodes[biddyNodeTable.blocksize-2].list = NULL;
4610  biddyNodeTable.generated = biddyNodeTable.blocksize;
4611  biddyNodeTable.blocknumber = 1;
4612 
4613  /* MAKE TERMINAL NODE "1" */
4614  /* TERMINAL NODE IS "1" FOR ALL BDD TYPES AND IT IS AT INDEX [0] */
4615  biddyNodeTable.table[0]->prev = NULL;
4616  biddyNodeTable.table[0]->next = NULL;
4617  biddyNodeTable.table[0]->list = NULL;
4618  biddyNodeTable.table[0]->f = biddyNull;
4619  biddyNodeTable.table[0]->t = biddyNull;
4620  biddyNodeTable.table[0]->v = 0; /* terminal node is the only one with v = 0 */
4621  biddyNodeTable.table[0]->expiry = 0; /* terminal node is fortified */
4622  biddyNodeTable.table[0]->select = 0; /* initialy it is not selected */
4623 
4624  /* MAKE TERMINAL EDGE AND EDGES REPRESENTING CONSTANTS */
4625  /* FOR THE EMPTY DOMAIN, biddyZero AND biddyOne ARE THE SAME FOR ALL BDD TYPES */
4626  /* biddyTerminal IS "1" FOR ALL BDD TYPES, INCLUDING OBDD, ZBDD, AND TZBDD */
4627  /* biddyZero IS COMPLEMENTED FOR ALL BDD TYPES, INCLUDING OBDD, ZBDD, AND TZBDD */
4628  MNG[2] = (void *) biddyNodeTable.table[0]; /* biddyTerminal */
4629  MNG[3] = BiddyComplement(biddyTerminal); /* biddyZero */
4630  MNG[4] = biddyTerminal; /* biddyOne */
4631 
4632  /* DEBUGGING */
4633  /*
4634  printf("DEBUG (BiddyInitMNG): biddyOne = %p\n",biddyOne);
4635  printf("DEBUG (BiddyInitMNG): biddyZero = %p\n",biddyZero);
4636  */
4637 
4638  /* INITIALIZATION OF VARIABLE'S VALUES */
4639  biddyVariableTable.table[0].value = biddyZero;
4640  for (i=1; i<biddyVariableTable.size; i++) {
4641  biddyVariableTable.table[i].value = biddyZero;
4642  }
4643 
4644  /* INITIALIZATION OF NODE SELECTION */
4645  biddySelect = 1;
4646 
4647  /* INITIALIZATION OF GARBAGE COLLECTION */
4648  /* MINIMAL VALUE FOR biddySystemAge IS 2 (SEE IMPLEMENTATION OF SIFTING) */
4649  biddySystemAge = 2;
4650 
4651  /* INITIALIZE FORMULA TABLE */
4652  /* first formula is 0, it is always a single terminal node */
4653  /* second formula is 1, it could be a large graph, e.g. for ZBDD */
4654  biddyFormulaTable.deletedName = strdup("BIDDY_DELETED_FORMULA");
4655  biddyFormulaTable.size = 2;
4656  biddyFormulaTable.numOrdered = 2;
4657  if (!(biddyFormulaTable.table = (BiddyFormula *)
4658  malloc(biddyFormulaTable.size*sizeof(BiddyFormula))))
4659  {
4660  fprintf(stderr,"BiddyInitMNG (formula table): Out of memoy!\n");
4661  exit(1);
4662  }
4663  biddyFormulaTable.table[0].name = strdup("0");
4664  biddyFormulaTable.table[0].f = biddyZero;
4665  biddyFormulaTable.table[0].expiry = 0;
4666  biddyFormulaTable.table[0].deleted = FALSE;
4667  biddyFormulaTable.table[1].name = strdup("1");
4668  biddyFormulaTable.table[1].f = biddyOne;
4669  biddyFormulaTable.table[1].expiry = biddySystemAge;
4670  biddyFormulaTable.table[1].deleted = FALSE;
4671 
4672  /* INITIALIZATION OF NODE TABLE */
4673  biddyNodeTable.max = 1;
4674  biddyNodeTable.num = 1;
4675  biddyNodeTable.garbage = 0;
4676  biddyNodeTable.swap = 0;
4677  biddyNodeTable.sifting = 0;
4678  biddyNodeTable.nodetableresize = 0;
4679  biddyNodeTable.funite = 0;
4680  biddyNodeTable.funandor = 0;
4681  biddyNodeTable.funxor = 0;
4682  biddyNodeTable.gctime = 0;
4683  biddyNodeTable.drtime = 0;
4684 #ifdef BIDDYEXTENDEDSTATS_YES
4685  biddyNodeTable.foa = 0;
4686  biddyNodeTable.find = 0;
4687  biddyNodeTable.compare = 0;
4688  biddyNodeTable.add = 0;
4689  biddyNodeTable.iterecursive = 0;
4690  biddyNodeTable.andorrecursive = 0;
4691  biddyNodeTable.xorrecursive = 0;
4692  biddyNodeTable.gcobsolete = NULL;
4693 #endif
4694 
4695  /* INITIALIZATION OF CACHE LIST */
4696  biddyCacheList = NULL;
4697 
4698  /* INITIALIZATION OF DEFAULT OPERATION CACHE - USED FOR ITE AND OTHER BOOLEAN OPERATIONS */
4699  biddyOPCache.disabled = FALSE;
4700  *(biddyOPCache.notusedyet) = TRUE;
4701 #ifdef BIDDYEXTENDEDSTATS_YES
4702  *(biddyOPCache.search) = *(biddyOPCache.find) = 0;
4703  *(biddyOPCache.insert) = *(biddyOPCache.overwrite) = 0;
4704 #endif
4705  if (!(biddyOPCache.table = (BiddyOp3Cache *)
4706  calloc((biddyOPCache.size+1),sizeof(BiddyOp3Cache)))) {
4707  fprintf(stderr,"BiddyInitMNG (OP cache): Out of memoy!\n");
4708  exit(1);
4709  }
4710  /* for (i=0;i<=biddyOPCache.size;i++) biddyOPCache.table[i].result = biddyNull; */
4711  BiddyManagedAddCache(MNG,BiddyOPGarbage);
4712 
4713  /* INITIALIZATION OF DEFAULT EA CACHE - USED FOR QUANTIFICATIONS */
4714  biddyEACache.disabled = FALSE;
4715  *(biddyEACache.notusedyet) = TRUE;
4716 #ifdef BIDDYEXTENDEDSTATS_YES
4717  *(biddyEACache.search) = *(biddyEACache.find) = 0;
4718  *(biddyEACache.insert) = *(biddyEACache.overwrite) = 0;
4719 #endif
4720  if (!(biddyEACache.table = (BiddyOp3Cache *)
4721  calloc((biddyEACache.size+1),sizeof(BiddyOp3Cache)))) {
4722  fprintf(stderr,"BiddyInitMNG (EA cache): Out of memoy!\n");
4723  exit(1);
4724  }
4725  /* for (i=0;i<=biddyEACache.size;i++) biddyEACache.table[i].result = biddyNull; */
4726  BiddyManagedAddCache(MNG,BiddyEAGarbage);
4727 
4728  /* INITIALIZATION OF DEFAULT RC CACHE - USED FOR RESTRICT AND COMPOSE */
4729  biddyRCCache.disabled = FALSE;
4730  *(biddyRCCache.notusedyet) = TRUE;
4731 #ifdef BIDDYEXTENDEDSTATS_YES
4732  *(biddyRCCache.search) = *(biddyRCCache.find) = 0;
4733  *(biddyRCCache.insert) = *(biddyRCCache.overwrite) = 0;
4734 #endif
4735  if (!(biddyRCCache.table = (BiddyOp3Cache *)
4736  calloc((biddyRCCache.size+1),sizeof(BiddyOp3Cache)))) {
4737  fprintf(stderr,"BiddyInitMNG (RC cache): Out of memoy!\n");
4738  exit(1);
4739  }
4740  /* for (i=0;i<=biddyRCCache.size;i++) biddyRCCache.table[i].result = biddyNull; */
4741  BiddyManagedAddCache(MNG,BiddyRCGarbage);
4742 
4743  /* INITIALIZATION OF DEFAULT REPLACE CACHE - USED FOR REPLACE */
4744  biddyReplaceCache.keywordList = NULL;
4745  biddyReplaceCache.keyList = NULL;
4746  biddyReplaceCache.keyNum = 0;
4747  biddyReplaceCache.keywordNum = 0;
4748  biddyReplaceCache.disabled = FALSE;
4749  *(biddyReplaceCache.notusedyet) = TRUE;
4750 #ifdef BIDDYEXTENDEDSTATS_YES
4751  *(biddyReplaceCache.search) = *(biddyReplaceCache.find) = 0;
4752  *(biddyReplaceCache.insert) = *(biddyReplaceCache.overwrite) = 0;
4753 #endif
4754  if (!(biddyReplaceCache.table = (BiddyKeywordCache *)
4755  calloc((biddyReplaceCache.size+1),sizeof(BiddyKeywordCache)))) {
4756  fprintf(stderr,"BiddyInitMNG (Replace cache): Out of memoy!\n");
4757  exit(1);
4758  }
4759  /* for (i=0;i<=biddyReplaceCache.size;i++) biddyReplaceCache.table[i].result = biddyNull; */
4760  BiddyManagedAddCache(MNG,BiddyReplaceGarbage);
4761 
4762  /* DEBUGGING */
4763  /*
4764  debugORDERING(MNG,biddyOrderingTable,biddyVariableTable.num);
4765  */
4766 
4767  /* DEBUGGING */
4768  /*
4769  BiddySystemReport(MNG);
4770  */
4771 
4772  /* DEBUGGING WITH GDB AND DDD */
4773  /* USE "up" TO CHANGE CONTEXT */
4774  /* use "print sizeof(BiddyNode)" */
4775  /* use "print sizeof(((BiddyNode *) biddyOne).f)" */
4776  /* use "graph display *((BiddyNode *) biddyOne)" */
4777  /* use "print ((BiddyNode *) biddyOne)" */
4778  /* use "print ((BiddyNode *) (((uintptr_t) f) & (~((uintptr_t) 1))))->v */
4779  /* use "print ((BiddyNode *) ((BiddyNode *) (((uintptr_t) f) & (~((uintptr_t) 1))))->f)->v" */
4780  /* use "print ((BiddyNode *) ((BiddyNode *) (((uintptr_t) f) & (~((uintptr_t) 1))))->t)->v" */
4781  /* use "print biddyVariableTable.table[0].name" */
4782 }
4783 
4784 /***************************************************************************/
4793 void
4794 BiddyExitMNG(Biddy_Manager *mng)
4795 {
4796  unsigned int i;
4797  BiddyCacheList *sup1, *sup2;
4798  Biddy_Manager MNG;
4799 
4800  if (!mng) {
4801  MNG = biddyAnonymousManager;
4802  } else {
4803  MNG = *mng;
4804  }
4805 
4806  /* REPORT ABOUT THE SYSTEM */
4807  /* CHECKING THE CORRECTNESS AND THE EFFICIENCY OF MEMORY MANAGEMENT */
4808 
4809  /*
4810 #ifdef BIDDYEXTENDEDSTATS_YES
4811  BiddySystemReport(MNG);
4812  printf("Number of ITE calls: %u (internal direct and recursive calls: %llu)\n",biddyNodeTable.funite,biddyNodeTable.iterecursive);
4813  printf("Number of AND and OR calls: %u (internal direct and recursive calls: %llu)\n",biddyNodeTable.funandor,biddyNodeTable.andorrecursive);
4814  printf("Number of XOR calls: %u (internal direct and recursive calls: %llu)\n",biddyNodeTable.funxor,biddyNodeTable.xorrecursive);
4815 #ifdef MINGW
4816  printf("Memory in use: %I64u bytes\n",BiddyManagedReadMemoryInUse(MNG));
4817 #else
4818  printf("Memory in use: %llu bytes\n",BiddyManagedReadMemoryInUse(MNG));
4819 #endif
4820  printf("Garbage collections so far: %u (node table resizing so far: %u)\n",biddyNodeTable.garbage,biddyNodeTable.nodetableresize);
4821  printf("Total time for garbage collections so far: %.3fs\n",biddyNodeTable.gctime / (1.0 * CLOCKS_PER_SEC));
4822  printf("Used buckets in node table: %u (%.2f%%)\n",
4823  BiddyManagedListUsed(MNG),
4824  (100.0*BiddyManagedListUsed(MNG)/(biddyNodeTable.size+1)));
4825  printf("Peak number of live BDD nodes: %u\n",biddyNodeTable.max);
4826  printf("Number of live BDD nodes: %u\n",biddyNodeTable.num);
4827  printf("Number of compared nodes: %llu (%.2f per findNodeTable call)\n",
4828  biddyNodeTable.compare,
4829  biddyNodeTable.find ?
4830  (1.0*biddyNodeTable.compare/biddyNodeTable.find):0);
4831 #endif
4832  */
4833 
4834  /*
4835  printf("Delete name and type...\n");
4836  */
4837  free(biddyManagerName); /* MNG[0] is not derefenced by macro */
4838 
4839  /*
4840  printf("Delete BDD type ...\n");
4841  */
4842  free((short int*)(MNG[1]));
4843 
4844  MNG[2] = NULL; /* biddyTerminal */
4845  MNG[3] = NULL; /* biddyZero */
4846  MNG[4] = NULL; /* biddyOne */
4847 
4848  /*
4849  printf("Delete nodes, block table, and node table...\n");
4850  */
4851  if ((BiddyNodeTable*)(MNG[5])) {
4852  for (i = 0; i < biddyNodeTable.blocknumber; i++) {
4853  free(biddyNodeTable.blocktable[i]);
4854  }
4855  free(biddyNodeTable.blocktable);
4856  free(biddyNodeTable.table);
4857 #ifdef BIDDYEXTENDEDSTATS_YES
4858  free(biddyNodeTable.gcobsolete);
4859 #endif
4860  free((BiddyNodeTable*)(MNG[5]));
4861  }
4862 
4863  /* TO DO: REMOVE VARIABLE NAMES FROM VARIABLE TABLE! */
4864  /*
4865  printf("Delete variable table...\n");
4866  */
4867  if ((BiddyVariableTable*)(MNG[6])) {
4868  free(biddyVariableTable.table);
4869  free(biddyVariableTable.lookup);
4870  free((BiddyVariableTable*)(MNG[6]));
4871  }
4872 
4873  /* TO DO: REMOVE FORMULAE NAMES! */
4874  /*
4875  printf("Delete formula table...\n");
4876  */
4877  if ((BiddyFormulaTable*)(MNG[7])) {
4878  free(biddyFormulaTable.table);
4879  free(biddyFormulaTable.deletedName);
4880  free((BiddyFormulaTable*)(MNG[7]));
4881  }
4882 
4883  /*
4884  printf("Delete OP cache...\n");
4885  */
4886  if ((BiddyOp3CacheTable*)(MNG[8])) {
4887  free(biddyOPCache.table);
4888  free(biddyOPCache.notusedyet);
4889 #ifdef BIDDYEXTENDEDSTATS_YES
4890  free(biddyOPCache.search);
4891  free(biddyOPCache.find);
4892  free(biddyOPCache.insert);
4893  free(biddyOPCache.overwrite);
4894 #endif
4895  free((BiddyOp3CacheTable*)(MNG[8]));
4896  }
4897 
4898  /*
4899  printf("Delete EA cache...\n");
4900  */
4901  if ((BiddyOp3CacheTable*)(MNG[9])) {
4902  free(biddyEACache.table);
4903  free(biddyEACache.notusedyet);
4904 #ifdef BIDDYEXTENDEDSTATS_YES
4905  free(biddyEACache.search);
4906  free(biddyEACache.find);
4907  free(biddyEACache.insert);
4908  free(biddyEACache.overwrite);
4909 #endif
4910  free((BiddyOp3CacheTable*)(MNG[9]));
4911  }
4912 
4913  /*
4914  printf("Delete RC cache...\n");
4915  */
4916  if ((BiddyOp3CacheTable*)(MNG[10])) {
4917  free(biddyRCCache.table);
4918  free(biddyRCCache.notusedyet);
4919 #ifdef BIDDYEXTENDEDSTATS_YES
4920  free(biddyRCCache.search);
4921  free(biddyRCCache.find);
4922  free(biddyRCCache.insert);
4923  free(biddyRCCache.overwrite);
4924 #endif
4925  free((BiddyOp3CacheTable*)(MNG[10]));
4926  }
4927 
4928  /*
4929  printf("Delete Replace cache...\n");
4930  */
4931  if ((BiddyKeywordCacheTable*)(MNG[11])) {
4932  for (i = 0; i < biddyReplaceCache.keywordNum; i++) {
4933  free(biddyReplaceCache.keywordList[i]);
4934  }
4935  free(biddyReplaceCache.keywordList);
4936  free(biddyReplaceCache.keyList);
4937  free(biddyReplaceCache.table);
4938  free(biddyReplaceCache.notusedyet);
4939 #ifdef BIDDYEXTENDEDSTATS_YES
4940  free(biddyReplaceCache.search);
4941  free(biddyReplaceCache.find);
4942  free(biddyReplaceCache.insert);
4943  free(biddyReplaceCache.overwrite);
4944 #endif
4945  free((BiddyKeywordCacheTable*)(MNG[11]));
4946  }
4947 
4948  /*
4949  printf("Delete cache list...\n");
4950  */
4951  if ((BiddyCacheList**)(MNG[12])) {
4952  sup1 = biddyCacheList;
4953  while (sup1) {
4954  sup2 = sup1->next;
4955  free(sup1);
4956  sup1 = sup2;
4957  }
4958  free((BiddyCacheList**)(MNG[12]));
4959  }
4960 
4961  /*
4962  printf("Delete pointer biddyFreeNodes...\n");
4963  */
4964  free((BiddyNode**)(MNG[13]));
4965 
4966  /*
4967  printf("Delete Ordering table...\n");
4968  */
4969  free((BiddyOrderingTable*)(MNG[14]));
4970 
4971  /*
4972  printf("Delete age...\n");
4973  */
4974  free((unsigned int*)(MNG[15]));
4975 
4976  /*
4977  printf("Delete selector...\n");
4978  */
4979  free((unsigned short int*)(MNG[16]));
4980 
4981  /*
4982  printf("And finally, delete manager...\n");
4983  */
4984  free((BiddyManager*)MNG);
4985 
4986  /* USER SHOULD DELETE HIS OWN CACHES */
4987 }
4988 
4989 /***************************************************************************/
4999 BiddyAbout()
5000 {
5001  return strdup(BIDDYVERSION);
5002 }
5003 
5004 /***************************************************************************/
5013 /* TO DO: replace with macro */
5015 BiddyManagedIsOK(Biddy_Manager MNG, Biddy_Edge f)
5016 {
5017  assert( MNG );
5018 
5019  return (!(BiddyN(f)->expiry) || ((BiddyN(f)->expiry) >= biddySystemAge));
5020 }
5021 
5022 /***************************************************************************/
5031 int
5032 BiddyManagedGetManagerType(Biddy_Manager MNG)
5033 {
5034  assert( MNG );
5035 
5036  return biddyManagerType;
5037 }
5038 
5039 /***************************************************************************/
5049 BiddyManagedGetManagerName(Biddy_Manager MNG)
5050 {
5051  assert( MNG );
5052 
5053  return biddyManagerName;
5054 }
5055 
5056 /***************************************************************************/
5065 void
5066 BiddyManagedSetManagerParameters(Biddy_Manager MNG, float gcr, float gcrF,
5067  float gcrX, float rr, float rrF, float rrX, float st, float cst)
5068 {
5069  assert( MNG );
5070 
5071  if (gcr > 0.0) biddyNodeTable.gcratio = gcr;
5072  if (gcrF > 0.0) biddyNodeTable.gcratioF = gcrF;
5073  if (gcrX > 0.0) biddyNodeTable.gcratioX = gcrX;
5074  if (rr > 0.0) biddyNodeTable.resizeratio = rr;
5075  if (rrF > 0.0) biddyNodeTable.resizeratioF = rrF;
5076  if (rrX > 0.0) biddyNodeTable.resizeratioX = rrX;
5077  if (st > 0.0) biddyNodeTable.siftingtreshold = st;
5078  if (cst > 0.0) biddyNodeTable.convergesiftingtreshold = cst;
5079 
5080  /* PROFILING */
5081  /*
5082  fprintf(stderr,"gcr=%.2f, ",biddyNodeTable.gcratio);
5083  fprintf(stderr,"gcrF=%.2f, ",biddyNodeTable.gcratioF);
5084  fprintf(stderr,"gcrX=%.2f, ",biddyNodeTable.gcratioX);
5085  fprintf(stderr,"rr=%.2f, ",biddyNodeTable.resizeratio);
5086  fprintf(stderr,"rrF=%.2f, ",biddyNodeTable.resizeratioF);
5087  fprintf(stderr,"rrX=%.2f, ",biddyNodeTable.resizeratioX);
5088  */
5089 }
5090 
5091 /***************************************************************************/
5100 Biddy_Edge
5101 BiddyManagedGetBaseSet(Biddy_Manager MNG)
5102 {
5103  Biddy_Edge r;
5104  Biddy_Variable v;
5105 #ifndef COMPACT
5106  Biddy_Variable top;
5107 #endif
5108 
5109  assert( MNG );
5110 
5111  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
5112  assert(
5113  (biddyManagerType == BIDDYTYPEOBDD) ||
5114  (biddyManagerType == BIDDYTYPEOBDDC) ||
5115  (biddyManagerType == BIDDYTYPEZBDD) ||
5116  (biddyManagerType == BIDDYTYPEZBDDC) ||
5117  (biddyManagerType == BIDDYTYPETZBDD)
5118  );
5119 
5120  r = biddyNull;
5121 
5122  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
5123  r = biddyOne;
5124  for (v=1;v<biddyVariableTable.num;v++) {
5125  r = BiddyManagedITE(MNG,biddyVariableTable.table[v].variable,biddyZero,r);
5126  }
5127  }
5128 #ifndef COMPACT
5129  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
5130  r = biddyTerminal;
5131  } else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
5132  /* r depends on topmost variable */
5133  top = 0;
5134  for (v = 1; v < biddyVariableTable.num; v++) {
5135  top = biddyVariableTable.table[top].prev;
5136  }
5137  r = biddyTerminal;
5138  BiddySetTag(r,top);
5139  }
5140 #endif
5141  return r;
5142 }
5143 
5144 /***************************************************************************/
5153 Biddy_Edge
5154 BiddyManagedTransferMark(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean mark,
5155  Biddy_Boolean leftright)
5156 {
5157  assert( MNG );
5158 
5159  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
5160  assert(
5161  (biddyManagerType == BIDDYTYPEOBDD) ||
5162  (biddyManagerType == BIDDYTYPEOBDDC) ||
5163  (biddyManagerType == BIDDYTYPEZBDD) ||
5164  (biddyManagerType == BIDDYTYPEZBDDC) ||
5165  (biddyManagerType == BIDDYTYPETZBDD)
5166  );
5167 
5168  if (biddyManagerType == BIDDYTYPEOBDDC) {
5169  if (BiddyGetMark(f) != mark) BiddySetMark(f); else BiddyClearMark(f);
5170  }
5171  else if (biddyManagerType == BIDDYTYPEOBDD) {
5172  /* NOTHING TO TRANSFER */
5173  }
5174 #ifndef COMPACT
5175  else if (biddyManagerType == BIDDYTYPEZBDDC) {
5176  if (leftright) {
5177  if (BiddyGetMark(f) != mark) BiddySetMark(f); else BiddyClearMark(f);
5178  }
5179  }
5180  else if ((biddyManagerType == BIDDYTYPEZBDD) ||
5181  (biddyManagerType == BIDDYTYPETZBDD))
5182  {
5183  /* NOTHING TO TRANSFER */
5184  }
5185 #endif
5186  else if (leftright) {
5187  /* MAKE COMPILER HAPPY */
5188  }
5189 
5190  return f;
5191 }
5192 
5193 /***************************************************************************/
5203 BiddyManagedIsEqv(Biddy_Manager MNG1, Biddy_Edge f1, Biddy_Manager MNG2,
5204  Biddy_Edge f2)
5205 {
5206  Biddy_Boolean r;
5207 
5208  assert( MNG1 );
5209  assert( biddyManagerType1 == biddyManagerType2 );
5210 
5211  if (MNG1 == MNG2) return (f1 == f2);
5212 
5213  r = isEqv(MNG1,f1,MNG2,f2);
5214  BiddyManagedDeselectAll(MNG1);
5215 
5216  return r;
5217 }
5218 
5219 /***************************************************************************/
5228 void
5229 BiddyManagedSelectNode(Biddy_Manager MNG, Biddy_Edge f)
5230 {
5231  assert( MNG );
5232 
5233  ((BiddyNode *) BiddyP(f))->select = biddySelect;
5234 }
5235 
5236 /***************************************************************************/
5245 void
5246 BiddyManagedDeselectNode(Biddy_Manager MNG, Biddy_Edge f)
5247 {
5248  assert( MNG );
5249 
5250  ((BiddyNode *) BiddyP(f))->select = 0;
5251 }
5252 
5253 /***************************************************************************/
5263 BiddyManagedIsSelected(Biddy_Manager MNG, Biddy_Edge f)
5264 {
5265  assert( MNG );
5266 
5267  return (((BiddyNode *) BiddyP(f))->select == biddySelect);
5268 }
5269 
5270 /***************************************************************************/
5279 void
5280 BiddyManagedSelectFunction(Biddy_Manager MNG, Biddy_Edge f)
5281 {
5282  assert( MNG );
5283 
5284  /* VARIANT 1 - ITERATIVE */
5285  /*
5286  BiddyNode **stack;
5287  BiddyNode **SP;
5288  BiddyNode *p;
5289  if ((p=(BiddyNode *) BiddyP(f))->select != biddySelect) {
5290  SP = stack = (BiddyNode **)
5291  malloc(biddyNodeTable.num * sizeof(BiddyNode *));
5292  *(SP++) = p;
5293  while (SP != stack) {
5294  p = (*(--SP));
5295  p->select = biddySelect;
5296  if (((BiddyNode *) BiddyP(p->f))->select != biddySelect) {
5297  *(SP++) = (BiddyNode *) BiddyP(p->f);
5298  }
5299  if (((BiddyNode *) p->t)->select != biddySelect) {
5300  *(SP++) = (BiddyNode *) p->t;
5301  }
5302  }
5303  free(stack);
5304  }
5305  */
5306 
5307  /* VARIANT 2 - RECURSIVE */
5308 
5309  if (((BiddyNode *)BiddyP(f))->select != biddySelect) {
5310  ((BiddyNode *)BiddyP(f))->select = biddySelect;
5311  BiddyManagedSelectFunction(MNG,BiddyE(f));
5312  BiddyManagedSelectFunction(MNG,BiddyT(f));
5313  }
5314 
5315 
5316 }
5317 
5318 /***************************************************************************/
5327 void
5328 BiddyManagedDeselectAll(Biddy_Manager MNG)
5329 {
5330  assert( MNG );
5331 
5332  if (++biddySelect == 0) {
5333  /* biddySelect is back to start - explicite deselection is required */
5334  Biddy_Variable v;
5335  BiddyNode *sup;
5336  biddyNodeTable.table[0]->select = 0;
5337  for (v=1; v<biddyVariableTable.num; v++) {
5338  biddyVariableTable.table[v].lastNode->list = NULL;
5339  sup = biddyVariableTable.table[v].firstNode;
5340  assert( sup != NULL );
5341  while (sup) {
5342  assert(sup->v == v) ;
5343  sup->select = 0;
5344  sup = (BiddyNode *) sup->list;
5345  }
5346  }
5347  biddySelect = 1;
5348  }
5349 }
5350 
5351 /***************************************************************************/
5361 BiddyManagedGetVariable(Biddy_Manager MNG, Biddy_String x)
5362 {
5363  Biddy_Variable v,min,max;
5364  Biddy_Boolean find;
5365  int cc;
5366 
5367  assert( MNG );
5368 
5369  /* VARIABLE TABLE IS NEVER EMPTY. AT LEAST, THERE IS ELEMENT '1' AT INDEX [0] */
5370 
5371  v = 0;
5372  find = FALSE;
5373 
5374  /* VARIANT A: SEARCH FOR THE VARIABLE IN THE ORIGINAL TABLE */
5375  /*
5376  while (!find && v<biddyVariableTable.num) {
5377  if ((x[0] == biddyVariableTable.table[v].name[0]) &&
5378  (!strcmp(x,biddyVariableTable.table[v].name)))
5379  {
5380  find = TRUE;
5381  } else {
5382  v++;
5383  }
5384  }
5385  */
5386 
5387  /* VARIANT B: SEARCH IN THE LOOKUP TABLE */
5388 
5389  min = 0;
5390  max = biddyVariableTable.num - 1;
5391  cc = strcmp(x,biddyVariableTable.lookup[min].name);
5392  if (cc == 0) {
5393  v = min;
5394  find = TRUE;
5395  } else if (cc < 0) {
5396  v = min;
5397  find = FALSE;
5398  } else {
5399  cc = strcmp(x,biddyVariableTable.lookup[max].name);
5400  if (cc == 0) {
5401  v = max;
5402  find = TRUE;
5403  } else if (cc > 0) {
5404  v = max+1;
5405  find = FALSE;
5406  } else {
5407  v = (min + max) / 2;
5408  while (v != min) {
5409  cc = strcmp(x,biddyVariableTable.lookup[v].name);
5410  if (cc == 0) {
5411  min = max = v;
5412  find = TRUE;
5413  } else if (cc < 0) {
5414  max = v;
5415  } else {
5416  min = v;
5417  }
5418  v = (min + max) / 2;
5419  }
5420  if (!find) v++;
5421  }
5422  }
5423  if (find) {
5424  v = biddyVariableTable.lookup[v].v;
5425  } else {
5426  v = 0;
5427  }
5428 
5429 
5430  /* IF find THEN v IS THE INDEX OF THE CORRECT ELEMENT! */
5431 
5432  return v;
5433 }
5434 
5435 /***************************************************************************/
5445 BiddyManagedGetLowestVariable(Biddy_Manager MNG)
5446 {
5447  Biddy_Variable v,k;
5448 
5449  assert( MNG );
5450 
5451  v = 0;
5452  for (k = 1; k < biddyVariableTable.num; k++) {
5453  v = biddyVariableTable.table[v].prev;
5454  }
5455 
5456  return v;
5457 }
5458 
5459 /***************************************************************************/
5469 BiddyManagedGetIthVariable(Biddy_Manager MNG, Biddy_Variable i)
5470 {
5471  Biddy_Variable v;
5472 
5473  assert( MNG );
5474 
5475  if ((i == 0) || (i > biddyVariableTable.num)) {
5476  return 0;
5477  } else {
5478  v = 0;
5479  while (i < biddyVariableTable.num) {
5480  v = BiddyManagedGetPrevVariable(MNG,v);
5481  i++;
5482  }
5483  }
5484 
5485  return v;
5486 }
5487 
5488 /***************************************************************************/
5498 BiddyManagedGetPrevVariable(Biddy_Manager MNG, Biddy_Variable v)
5499 {
5500  assert( MNG );
5501 
5502  if (v >= biddyVariableTable.num) {
5503  return 0;
5504  } else {
5505  return biddyVariableTable.table[v].prev;
5506  }
5507 }
5508 
5509 /***************************************************************************/
5519 BiddyManagedGetNextVariable(Biddy_Manager MNG, Biddy_Variable v)
5520 {
5521  assert( MNG );
5522 
5523  if (v >= biddyVariableTable.num) {
5524  return 0;
5525  } else {
5526  return biddyVariableTable.table[v].next;
5527  }
5528 }
5529 
5530 /***************************************************************************/
5539 Biddy_Edge
5540 BiddyManagedGetVariableEdge(Biddy_Manager MNG, Biddy_Variable v)
5541 {
5542  assert( MNG );
5543 
5544  return biddyVariableTable.table[v].variable;
5545 }
5546 
5547 /***************************************************************************/
5556 Biddy_Edge
5557 BiddyManagedGetElementEdge(Biddy_Manager MNG, Biddy_Variable v)
5558 {
5559  assert( MNG );
5560 
5561  return biddyVariableTable.table[v].element;
5562 }
5563 
5564 /***************************************************************************/
5574 BiddyManagedGetVariableName(Biddy_Manager MNG, Biddy_Variable v)
5575 {
5576  assert( MNG );
5577 
5578  return biddyVariableTable.table[v].name;
5579 }
5580 
5581 /***************************************************************************/
5590 Biddy_Edge
5591 BiddyManagedGetTopVariableEdge(Biddy_Manager MNG, Biddy_Edge f)
5592 {
5593  assert( MNG );
5594 
5595  assert( f != NULL );
5596 
5597  return biddyVariableTable.table[BiddyV(f)].variable;
5598 }
5599 
5600 /***************************************************************************/
5610 BiddyManagedGetTopVariableName(Biddy_Manager MNG, Biddy_Edge f)
5611 {
5612  assert( MNG );
5613 
5614  assert( f != NULL );
5615 
5616  return biddyVariableTable.table[BiddyV(f)].name;
5617 }
5618 
5619 /***************************************************************************/
5628 char
5629 BiddyManagedGetTopVariableChar(Biddy_Manager MNG, Biddy_Edge f)
5630 {
5631  assert( MNG );
5632 
5633  assert( f != NULL );
5634 
5635  return biddyVariableTable.table[BiddyV(f)].name[0];
5636 }
5637 
5638 /***************************************************************************/
5647 void
5648 BiddyManagedResetVariablesValue(Biddy_Manager MNG)
5649 {
5650  Biddy_Variable v;
5651 
5652  assert( MNG );
5653 
5654  for (v=0; v<biddyVariableTable.num; v++) {
5655  biddyVariableTable.table[v].value = biddyZero;
5656  }
5657 }
5658 
5659 /***************************************************************************/
5668 void
5669 BiddyManagedSetVariableValue(Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge f)
5670 {
5671  assert( MNG );
5672 
5673  biddyVariableTable.table[v].value = f;
5674 }
5675 
5676 /***************************************************************************/
5685 Biddy_Edge
5686 BiddyManagedGetVariableValue(Biddy_Manager MNG, Biddy_Variable v)
5687 {
5688  assert( MNG );
5689 
5690  return biddyVariableTable.table[v].value;
5691 }
5692 
5693 /***************************************************************************/
5702 void
5703 BiddyManagedClearVariablesData(Biddy_Manager MNG)
5704 {
5705  Biddy_Variable v;
5706 
5707  assert( MNG );
5708 
5709  for (v=0; v<biddyVariableTable.num; v++) {
5710  if (biddyVariableTable.table[v].data) {
5711  free(biddyVariableTable.table[v].data);
5712  biddyVariableTable.table[v].data = NULL;
5713  }
5714  }
5715 }
5716 
5717 /***************************************************************************/
5726 void
5727 BiddyManagedSetVariableData(Biddy_Manager MNG, Biddy_Variable v, void *x)
5728 {
5729  assert( MNG );
5730 
5731  biddyVariableTable.table[v].data = x;
5732 }
5733 
5734 /***************************************************************************/
5743 void *
5744 BiddyManagedGetVariableData(Biddy_Manager MNG, Biddy_Variable v)
5745 {
5746  assert( MNG );
5747 
5748  return biddyVariableTable.table[v].data;
5749 }
5750 
5751 /***************************************************************************/
5761 BiddyManagedEval(Biddy_Manager MNG, Biddy_Edge f)
5762 {
5763  Biddy_Boolean r;
5764  Biddy_Variable fv,ftop;
5765 
5766  assert( MNG );
5767 
5768  assert( f != NULL );
5769 
5770  if (f == biddyNull) return FALSE;
5771 
5772  ftop = 0;
5773  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
5774  ftop = BiddyV(f);
5775  }
5776 #ifndef COMPACT
5777  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
5778  /* determine the topmost variable (for ZBDDs, it has prev=biddyVariableTable.num) */
5779  ftop = BiddyV(f);
5780  while (biddyVariableTable.table[ftop].prev != biddyVariableTable.num) {
5781  ftop = biddyVariableTable.table[ftop].prev;
5782  }
5783  } else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
5784  ftop = BiddyGetTag(f);
5785  }
5786 #endif
5787 
5788  r = !(BiddyGetMark(f));
5789  while (ftop != 0) {
5790 
5791  fv = BiddyV(f);
5792  assert( biddyVariableTable.table[fv].value != NULL );
5793 
5794  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
5795 
5796  if (biddyVariableTable.table[fv].value == biddyZero) {
5797  f = BiddyE(f);
5798  /* for OBDDC, 'else' successor can be marked */
5799  if (BiddyGetMark(f)) r = !r;
5800  } else {
5801  f = BiddyT(f);
5802  /* for OBDD, biddyZero is a marked edge to 'then' successor! */
5803  if (BiddyGetMark(f)) r = !r;
5804  }
5805  ftop = BiddyV(f);
5806 
5807  }
5808 
5809 #ifndef COMPACT
5810  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
5811 
5812  while (ftop != fv) {
5813  assert( biddyVariableTable.table[ftop].value != NULL );
5814  if (biddyVariableTable.table[ftop].value == biddyZero) {
5815  ftop = BiddyManagedGetNextVariable(MNG,ftop);
5816  } else {
5817  r = FALSE;
5818  ftop = fv = 0;
5819  }
5820  }
5821  if (fv != 0) {
5822  if (biddyVariableTable.table[fv].value == biddyZero) {
5823  f = BiddyE(f);
5824  /* for ZBDD, biddyZero is a marked edge to 'else' successor! */
5825  if (BiddyGetMark(f)) r = !r;
5826  } else {
5827  f = BiddyT(f);
5828  /* for ZBDDC, mark is transfered only to the left successor */
5829  r = TRUE;
5830  /* for ZBDDC, 'then' successor can be marked */
5831  if (BiddyGetMark(f)) r = !r;
5832  }
5833  ftop = BiddyManagedGetNextVariable(MNG,fv);
5834  }
5835 
5836  } else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
5837 
5838  while (ftop != fv) {
5839  assert( biddyVariableTable.table[ftop].value != NULL );
5840  if (biddyVariableTable.table[ftop].value == biddyZero) {
5841  ftop = BiddyManagedGetNextVariable(MNG,ftop);
5842  } else {
5843  r = FALSE;
5844  ftop = fv = 0;
5845  }
5846  }
5847  if (fv != 0) {
5848  if (biddyVariableTable.table[fv].value == biddyZero) {
5849  f = BiddyE(f);
5850  /* for TZBDD, marks are not transfered but used only to denote 0 */
5851  if (BiddyGetMark(f)) r = FALSE;
5852  } else {
5853  f = BiddyT(f);
5854  /* for TZBDD, marks are not transfered but used only to denote 0 */
5855  if (BiddyGetMark(f)) r = FALSE;
5856  }
5857  ftop = BiddyGetTag(f);
5858  }
5859  }
5860 #endif
5861 
5862  }
5863 
5864  return r;
5865 }
5866 
5867 /***************************************************************************/
5876 double
5877 BiddyManagedEvalProbability(Biddy_Manager MNG, Biddy_Edge f)
5878 {
5879  double r1,r0;
5880  Biddy_Boolean rf;
5881 
5882  assert( MNG );
5883 
5884  if (BiddyIsNull(f)) return 0;
5885  if (f == biddyZero) return 0;
5886  if (BiddyIsTerminal(f)) return 1;
5887 
5888  BiddyCreateLocalInfo(MNG,f);
5889  evalProbability(MNG,f,&r1,&r0,&rf); /* all nodes except terminal node are selected */
5890  BiddyDeleteLocalInfo(MNG,f);
5891 
5892  return r1;
5893 }
5894 
5895 /***************************************************************************/
5915 BiddyManagedFoaVariable(Biddy_Manager MNG, Biddy_String x,
5916  Biddy_Boolean varelem, Biddy_Boolean complete)
5917 {
5918  unsigned int i,min,max;
5919  Biddy_Variable v,w;
5920  int cc;
5921  Biddy_Boolean isNumbered,find;
5922  Biddy_String tmp;
5923  unsigned int expiry;
5924 
5925  assert( MNG );
5926 
5927  v = 0;
5928  isNumbered = FALSE;
5929  find = FALSE;
5930  if (!x) {
5931 
5932  biddyVariableTable.numnum++;
5933  if (!(x = (Biddy_String)malloc(15))) {
5934  fprintf(stderr, "BiddyManagedFoaVariable: Out of memoy!\n");
5935  exit(1);
5936  }
5937  sprintf(x,"%u",biddyVariableTable.numnum);
5938  v = biddyVariableTable.num;
5939  isNumbered = TRUE;
5940 
5941  }
5942 
5943  /* IF NAME LOOKS AS A NUMBER THEN ADAPT numnum TO AVOID PROBLEMS AFTER ADDING NUMBERED VARIABLES */
5944  if (x) {
5945 #ifdef PLAIN
5946  sscanf(x,"%u",&v);
5947 #else
5948  sscanf(x,"%hu",&v);
5949 #endif
5950  tmp = strdup(x);
5951 #ifdef PLAIN
5952  sprintf(tmp,"%u",v);
5953 #else
5954  sprintf(tmp,"%hu",v);
5955 #endif
5956  if (!strcmp(x,tmp)) {
5957  if (biddyVariableTable.numnum < v) biddyVariableTable.numnum = v;
5958  }
5959  free(tmp);
5960  }
5961 
5962  /* DEBUGGING */
5963  /*
5964  printf("BiddyManagedFoaVariable (%s, %p): adding new variable/element %s, biddyVariableTable.num = %u\n",BiddyManagedGetManagerName(MNG),MNG,x,biddyVariableTable.num);
5965  */
5966 
5967  /* SEARCH FOR THE EXISTING VARIABLE/ELEMENT/FORMULA WITH THE GIVEN NAME */
5968  /* FOR NUMBERED VARIABLE, WE KNOW THAT IT DOES NOT EXIST, BUT WE HAVE TO FIND INDEX IN LOOKUP TABLE */
5969  /* VARIABLE TABLE IS NEVER EMPTY. AT LEAST, THERE IS ELEMENT '1' AT INDEX [0] */
5970 
5971  /* VARIANT WITHOUT LOOKUP TABLE: SEARCH IN THE ORIGINAL TABLE */
5972  /*
5973  if (!isNumbered) {
5974  while (!find && v<biddyVariableTable.num) {
5975  if (!strcmp(x,biddyVariableTable.table[v].name)) {
5976  find = TRUE;
5977  } else {
5978  v++;
5979  }
5980  }
5981  }
5982  */
5983 
5984  min = 0;
5985  max = biddyVariableTable.num - 1;
5986  cc = strcmp(x,biddyVariableTable.lookup[min].name);
5987  if (cc == 0) {
5988  w = min;
5989  find = TRUE;
5990  } else if (cc < 0) {
5991  w = min;
5992  find = FALSE;
5993  } else {
5994  cc = strcmp(x,biddyVariableTable.lookup[max].name);
5995  if (cc == 0) {
5996  w = max;
5997  find = TRUE;
5998  } else if (cc > 0) {
5999  w = max+1;
6000  find = FALSE;
6001  } else {
6002  w = (min + max) / 2;
6003  while (w != min) {
6004  cc = strcmp(x,biddyVariableTable.lookup[w].name);
6005  if (cc == 0) {
6006  min = max = w;
6007  find = TRUE;
6008  } else if (cc < 0) {
6009  max = w;
6010  } else {
6011  min = w;
6012  }
6013  w = (min + max) / 2;
6014  }
6015  if (!find) w++;
6016  }
6017  }
6018  if (find) {
6019  v = biddyVariableTable.lookup[w].v;
6020  } else {
6021  v = biddyVariableTable.num;
6022  }
6023 
6024  /* IF (find == FALSE) THEN w IS THE INDEX OF THE NEW VARIABLE/ELEMENT IN LOOKUP TABLE */
6025  /* IF (find == TRUE) THEN v IS THE INDEX OF THE CORRECT VARIABLE/ELEMENT */
6026  /* IN THIS CASE, NEW VARIABLE IS NOT ADDED */
6027  if (!find) {
6028 
6029  /* SEARCH FOR THE EXISTING FORMULA WITH THE SAME NAME */
6030  /* FORMULAE IN FORMULA TABLE ARE ORDERED BY NAME */
6031  /* TO DO: USE THE SAME METHOD AS IN FindFormula */
6032  for (i = 0; !find && (i < biddyFormulaTable.numOrdered); i++) {
6033  if (biddyFormulaTable.table[i].name) {
6034  cc = strcmp(x,biddyFormulaTable.table[i].name);
6035  if ((cc == 0) && !biddyFormulaTable.table[i].deleted) {
6036  find = TRUE;
6037  break;
6038  }
6039  if (cc < 0) break;
6040  } else {
6041  fprintf(stderr,"BiddyManagedFoaVariable: Problem with the formula table!\n");
6042  exit(1);
6043  }
6044  }
6045  if (find) {
6046  printf("WARNING (BiddyManagedFoaVariable): new variable/element %s has the same name as an existing formula!\n",x);
6047  return 0;
6048  }
6049 
6050  /* addVariableElement creates variable and/or element and prolongs results */
6051  /* new element is added at the end of variable table */
6052  addVariableElement(MNG,x,varelem,complete);
6053  assert ( v == biddyVariableTable.num-1 );
6054 
6055  /* ADD VARIABLE/ELEMENT TO LOOKUP TABLE */
6056 
6057  memmove(&biddyVariableTable.lookup[w+1],&biddyVariableTable.lookup[w],(biddyVariableTable.num-w-1)*sizeof(BiddyLookupVariable));
6058  biddyVariableTable.lookup[w].name = biddyVariableTable.table[v].name;
6059  biddyVariableTable.lookup[w].v = v;
6060 
6061  /* DEBUGGING */
6062  /*
6063  printf("BiddyManagedFoaVariable: new variable/element %s added, w = %u, v= %u, \n",x,w,v);
6064  */
6065 
6066  /* FOR OBDDs AND OFDDs, NEW VARIABLE WAS ADDED BELOW OF ALL THE EXISTING ONES */
6067  /* FOR ZBDDs AND ZFDDs, NEW VARIABLE WAS ADDED ABOVE OF ALL THE EXISTING ONES */
6068  /* FOR TZBDDs AND TZFDDs, NEW VARIABLE WAS ADDED ABOVE OF ALL THE EXISTING ONES */
6069 
6070  /* BECAUSE OF THESE RULES, NO CACHE TABLES NEED TO BE ADAPTED IN ANY CASE */
6071  /* THIS IS TRUE FOR BOTH CASES, IF EITHER A VARIABLE OR AN ELEMENT ARE ADDED */
6072  /* FOR OBDDs AND OFDDs, NO CACHE TABLES NEED TO BE ADAPTED IN ANY CASE */
6073  /* FOR ZBDDs AND ZFDDs, NO CACHE TABLES NEED TO BE ADAPTED IN ANY CASE */
6074  /* FOR TZBDDs AND TZFDDs, ONLY RECORDS IN CACHE TABLES WHERE ONE OF TOP VARIABLE IS ABOVE THE NEW VARIABLE MAY BE WRONG! */
6075 
6076  /* *** ADAPTING FORMULAE biddyZero AND biddyOne THAT ARE BOOLEAN FUNCTIONS (NOT COMBINATION SETS)! *** */
6077  /* first formula is biddyZero, for OBDDs and OFDDs it is always a single terminal node */
6078  /* first formula is biddyZero, for ZBDDs and ZFDDs it is always a single terminal node */
6079  /* first formula is biddyZero, for TZBDDs and TZFDDs it is always a single terminal node */
6080  /* second formula is biddyOne, for OBDDs and OFDDs it is always a single terminal node */
6081  /* second formula is biddyOne, for ZBDDs and ZFDDs it could be a large graph */
6082  /* second formula is biddyOne, for TZBDDs and TZFDDs it is always a single terminal node */
6083 
6084  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
6085  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
6086  {
6087  /* FOR OBDDs AND OFDDs, FORMULAE MUST BE ADAPTED ONLY IF THEY REPRESENT COMBINATION SETS */
6088  /* THIS PART IS ABOUT REPAIRING FORMULAE biddyZero AND biddyOne, THUS NO ACTION IS NEEDED */
6089  }
6090 
6091 #ifndef COMPACT
6092  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
6093  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD))
6094  {
6095  /* FOR ZBDDs AND ZFDDs, FORMULAE MUST BE ADAPTED IF THEY REPRESENT BOOLEAN FUNCTIONS */
6096  /* THIS PART IS ABOUT REPAIRING FORMULA biddyOne, THUS AN ACTION IS NEEDED */
6097  if (BiddyIsSmaller(biddyOrderingTable,v,BiddyV(biddyFormulaTable.table[1].f))) {
6098  /* IF NEW VARIABLE IS ABOVE FORMULA TOP VARIABLE, DIRECT METHOD IS POSSIBLE */
6099  /* printf("BiddyManagedFoaVariable: updating formula %s (deleted = %u)\n",biddyFormulaTable.table[i].name, biddyFormulaTable.table[i].deleted); */
6100  expiry = BiddyN(biddyFormulaTable.table[1].f)->expiry;
6101  biddyFormulaTable.table[1].f =
6102  BiddyManagedTaggedFoaNode(MNG,v,
6103  biddyFormulaTable.table[1].f,biddyFormulaTable.table[1].f,v,TRUE); /* FoaNode returns an obsolete node! */
6104  BiddyProlongOne(biddyFormulaTable.table[1].f,expiry);
6105  } else {
6106  /* USE OPERATION E - IS THIS THE MOST EFFICIENT METHOD? */
6107  expiry = BiddyN(biddyFormulaTable.table[1].f)->expiry;
6108  biddyFormulaTable.table[1].f = BiddyManagedE(MNG,biddyFormulaTable.table[1].f,v);
6109  BiddyProlongOne(biddyFormulaTable.table[1].f,expiry);
6110  }
6111  MNG[4] = biddyFormulaTable.table[1].f; /* biddyOne must be updated */
6112  }
6113 #endif
6114 
6115 #ifndef COMPACT
6116  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
6117  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6118  {
6119  /* FOR TZBDDs AND TZFDDs, FORMULAE MUST BE ADAPTED REGARDLESS OF WHAT THEY REPRESENT */
6120  /* HOWEVER, THIS PART IS ABOUT REPAIRING FORMULAE biddyZero AND biddyOne, ONLY, AND NO ACTION IS NEEDED HERE */
6121  }
6122 #endif
6123 
6124  /* *** ADAPTING ALL OTHER FORMULAE - ONLY REPAIRING OF NAMED FORMULAE IS USEFUL *** */
6125 
6126  /* FOR OBDDs AND OFDDs, FORMULAE MUST BE ADAPTED ONLY IF THEY REPRESENT COMBINATION SETS */
6127  /* IT IS ASSUMED, THAT FORMULAE REPRESENT COMBINATION SETS IFF NEW ELEMENT WAS ADDED */
6128  /* ADDED NODES ARE FRESH NODES, TOP NODE REMAINS THE SAME expiry TAG AS ORIGINAL FORMULA */
6129  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
6130  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
6131  {
6132  if (!varelem) {
6133  for (i = 2; i < biddyFormulaTable.size; i++) {
6134  if (biddyFormulaTable.table[i].f && !biddyFormulaTable.table[i].deleted && biddyFormulaTable.table[i].name) {
6135  /* USE OPERATION GT - IS THIS THE MOST EFFICIENT METHOD? */
6136  /* OPERATION ELEMENTABSTRACT IS POSSIBLE, TOO - WOULD IT BE MORE EFFICIENT? */
6137  expiry = BiddyN(biddyFormulaTable.table[i].f)->expiry;
6138  biddyFormulaTable.table[i].f = BiddyManagedGt(MNG,biddyFormulaTable.table[i].f,biddyVariableTable.table[v].variable);
6139  BiddyProlongOne(biddyFormulaTable.table[i].f,expiry);
6140  }
6141  }
6142  }
6143  }
6144 
6145 #ifndef COMPACT
6146  /* FOR ZBDDs AND ZFDDs, FORMULAE MUST BE ADAPTED ONLY IF THEY REPRESENT BOOLEAN FUNCTIONS */
6147  /* IT IS ASSUMED, THAT FORMULAE REPRESENT BOOLEAN FUNCTIONS IFF NEW VARIABLE WAS ADDED */
6148  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
6149  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD))
6150  {
6151  if (varelem) {
6152  for (i = 2; i < biddyFormulaTable.size; i++) {
6153  if (biddyFormulaTable.table[i].f && !biddyFormulaTable.table[i].deleted && biddyFormulaTable.table[i].name) {
6154  if (BiddyIsSmaller(biddyOrderingTable,v,BiddyV(biddyFormulaTable.table[i].f))) {
6155  /* IF NEW VARIABLE IS ABOVE FORMULA TOP VARIABLE, DIRECT METHOD IS POSSIBLE */
6156  /* printf("BiddyManagedFoaVariable: updating formula %s (deleted = %u)\n",biddyFormulaTable.table[i].name, biddyFormulaTable.table[i].deleted); */
6157  expiry = BiddyN(biddyFormulaTable.table[i].f)->expiry;
6158  biddyFormulaTable.table[i].f =
6159  BiddyManagedTaggedFoaNode(MNG,v,
6160  biddyFormulaTable.table[i].f,biddyFormulaTable.table[i].f,v,TRUE); /* FoaNode returns an obsolete node! */
6161  BiddyProlongOne(biddyFormulaTable.table[i].f,expiry);
6162  } else {
6163  /* USE OPERATION E - IS THIS THE MOST EFFICIENT METHOD? */
6164  expiry = BiddyN(biddyFormulaTable.table[i].f)->expiry;
6165  biddyFormulaTable.table[i].f = BiddyManagedE(MNG,biddyFormulaTable.table[i].f,v);
6166  BiddyProlongOne(biddyFormulaTable.table[i].f,expiry);
6167  }
6168  }
6169  }
6170  }
6171  }
6172 #endif
6173 
6174 #ifndef COMPACT
6175  /* FOR TZBDDs AND TZFDDs, FORMULAE MUST BE ADAPTED REGARDLESS OF WHAT THEY REPRESENT */
6176  /* IT IS ASSUMED, THAT FORMULAE REPRESENT BOOLEAN FUNCTIONS IFF NEW VARIABLE WAS ADDED */
6177  /* IT IS ASSUMED, THAT FORMULAE REPRESENT COMBINATION SETS IFF NEW ELEMENT WAS ADDED */
6178  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
6179  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6180  {
6181  if (varelem) {
6182  /* BOOLEAN FUNCTION */
6183  /* USE OPERATION E - IS THIS THE MOST EFFICIENT METHOD? */
6184  for (i = 2; i < biddyFormulaTable.size; i++) {
6185  if (biddyFormulaTable.table[i].f && !biddyFormulaTable.table[i].deleted && biddyFormulaTable.table[i].name) {
6186  /* FOR BOOLEAN FUNCTIONS, IF FORMULA TOP TAG IS BELOW THE NEW VARIABLE, NO ACTION IS NEEDED */
6187  if (BiddyIsSmaller(biddyOrderingTable,BiddyGetTag(biddyFormulaTable.table[i].f),v)) {
6188  expiry = BiddyN(biddyFormulaTable.table[i].f)->expiry;
6189  biddyFormulaTable.table[i].f = BiddyManagedE(MNG,biddyFormulaTable.table[i].f,v);
6190  BiddyProlongOne(biddyFormulaTable.table[i].f,expiry);
6191  }
6192  }
6193  }
6194  } else {
6195  /* COMBINATION SET */
6196  /* USE OPERATION GT - IS THIS THE MOST EFFICIENT METHOD? */
6197  /* OPERATION ELEMENTABSTRACT IS POSSIBLE, TOO - WOULD IT BE MORE EFFICIENT? */
6198  for (i = 2; i < biddyFormulaTable.size; i++) {
6199  if (biddyFormulaTable.table[i].f && !biddyFormulaTable.table[i].deleted && biddyFormulaTable.table[i].name) {
6200  /* FOR COMBINATION SETS, IF FORMULA TOP TAG IS BELOW THE NEW VARIABLE, DIRECT METHOD IS POSSIBLE */
6201  if (BiddyIsSmaller(biddyOrderingTable,v,BiddyGetTag(biddyFormulaTable.table[i].f))) {
6202  BiddySetTag(biddyFormulaTable.table[i].f,v);
6203  } else {
6204  expiry = BiddyN(biddyFormulaTable.table[i].f)->expiry;
6205  biddyFormulaTable.table[i].f = BiddyManagedGt(MNG,biddyFormulaTable.table[i].f,biddyVariableTable.table[v].variable);
6206  BiddyProlongOne(biddyFormulaTable.table[i].f,expiry);
6207  }
6208  }
6209  }
6210  }
6211  }
6212 #endif
6213 
6214  /* *** ADAPTING VARIABLES AND ELEMENTS *** */
6215  /* *** VARIABLES AND ELEMENTS ARE NOT ADDED TO FORMULA TABLE */
6216 
6217  /* FOR OBDDs AND OFDDs, ALL THE EXISTING ELEMENTS MUST BE ADAPTED */
6218  /* FOR OBDDs AND OFDDs, NEW VARIABLE IS ADDED BELOW OF ALL THE EXISTING ONES */
6219  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
6220  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
6221  {
6222  for (w = 1; w < biddyVariableTable.num-1; w++) {
6223  /* USE OPERATION GT - - IS THIS THE MOST EFFICIENT METHOD? */
6224  /* OPERATION ELEMENTABSTRACT IS POSSIBLE, TOO - WOULD IT BE MORE EFFICIENT? */
6225  if (biddyVariableTable.table[w].element) {
6226  expiry = BiddyN(biddyVariableTable.table[w].element)->expiry;
6227  biddyVariableTable.table[w].element = BiddyManagedGt(MNG,biddyVariableTable.table[w].element,biddyVariableTable.table[v].variable);
6228  BiddyProlongOne(biddyVariableTable.table[w].element,expiry);
6229  }
6230  /* SIMPLY RECREATE ALL THE EXISTING ELEMENTS - NOT EFFICIENT */
6231  /*
6232  Biddy_Variable top;
6233  Biddy_Edge result;
6234  result = biddyOne;
6235  top = 0;
6236  while (top != BiddyManagedGetLowestVariable(MNG)) {
6237  top = biddyVariableTable.table[top].prev;
6238  if (top == w) {
6239  result = BiddyManagedTaggedFoaNode(MNG,top,biddyZero,result,top,TRUE);
6240  BiddyRefresh(result);
6241  } else {
6242  result = BiddyManagedTaggedFoaNode(MNG,top,result,biddyZero,top,TRUE);
6243  BiddyRefresh(result);
6244  }
6245  }
6246  biddyVariableTable.table[w].element = result;
6247  */
6248  }
6249  }
6250 
6251  /* FOR ZBDDs AND ZFDDs, ALL THE EXISTING VARIABLES MUST BE ADAPTED */
6252  /* FOR ZBDDs AND ZFDDs, NEW VARIABLE IS ADDED ABOVE OF ALL THE EXISTING ONES */
6253 #ifndef COMPACT
6254  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
6255  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD))
6256  {
6257  for (w = 1; w < biddyVariableTable.num-1; w++) {
6258  if (biddyVariableTable.table[w].variable) {
6259  /* USE OPERATION E - IS THIS THE MOST EFFICIENT METHOD? */
6260  if (BiddyIsSmaller(biddyOrderingTable,v,BiddyV(biddyVariableTable.table[w].variable))) {
6261  /* IF NEW VARIABLE IS ABOVE FORMULA TOP VARIABLE, DIRECT METHOD IS POSSIBLE */
6262  expiry = BiddyN(biddyVariableTable.table[w].variable)->expiry;
6263  biddyVariableTable.table[w].variable =
6264  BiddyManagedTaggedFoaNode(MNG,v,
6265  biddyVariableTable.table[w].variable,biddyVariableTable.table[w].variable,v,TRUE); /* FoaNode returns an obsolete node! */
6266  BiddyProlongOne(biddyVariableTable.table[w].variable,expiry);
6267  } else {
6268  expiry = BiddyN(biddyVariableTable.table[w].variable)->expiry;
6269  biddyVariableTable.table[w].variable = BiddyManagedE(MNG,biddyVariableTable.table[w].variable,v);
6270  BiddyProlongOne(biddyVariableTable.table[w].variable,expiry);
6271  }
6272  /* DEBUGGING */
6273  /*
6274  printf("top node of variable after updating: %s\n",BiddyManagedGetTopVariableName(MNG,biddyVariableTable.table[w].variable));
6275  */
6276  }
6277  }
6278  }
6279 #endif
6280 
6281  /* FOR TZBDDs AND TZFDDs, ALL THE EXISTING VARIABLES AND ELEMENTS MUST BE ADAPTED */
6282  /* FOR TZBDDs AND TZFDDs, NEW VARIABLE IS ADDED ABOVE OF ALL THE EXISTING ONES */
6283 #ifndef COMPACT
6284  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
6285  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6286  {
6287  for (w = 1; w < biddyVariableTable.num-1; w++) {
6288  if (biddyVariableTable.table[w].variable) {
6289  /* USE OPERATION E - IS THIS THE MOST EFFICIENT METHOD? */
6290  /* FOR BOOLEAN FUNCTIONS, IF FORMULA TOP TAG IS BELOW THE NEW VARIABLE, NO ACTION IS NEEDED */
6291  if (BiddyIsSmaller(biddyOrderingTable,BiddyGetTag(biddyVariableTable.table[w].variable),v)) {
6292  expiry = BiddyN(biddyVariableTable.table[w].variable)->expiry;
6293  biddyVariableTable.table[w].variable = BiddyManagedE(MNG,biddyVariableTable.table[w].variable,v);
6294  BiddyProlongOne(biddyVariableTable.table[w].variable,expiry);
6295  }
6296  }
6297  if (biddyVariableTable.table[w].element) {
6298  /* USE OPERATION GT - IS THIS THE MOST EFFICIENT METHOD? */
6299  /* OPERATION ELEMENTABSTRACT IS POSSIBLE, TOO - WOULD IT BE MORE EFFICIENT? */
6300  /* FOR COMBINATION SETS, IF FORMULA TOP TAG IS BELOW THE NEW VARIABLE, DIRECT METHOD IS POSSIBLE */
6301  if (BiddyIsSmaller(biddyOrderingTable,v,BiddyGetTag(biddyVariableTable.table[w].element))) {
6302  BiddySetTag(biddyVariableTable.table[w].element,v);
6303  } else {
6304  expiry = BiddyN(biddyVariableTable.table[w].element)->expiry;
6305  biddyVariableTable.table[w].element = BiddyManagedGt(MNG,biddyVariableTable.table[w].element,biddyVariableTable.table[v].variable);
6306  BiddyProlongOne(biddyVariableTable.table[w].element,expiry);
6307  }
6308  }
6309  }
6310  }
6311 #endif
6312 
6313  } else {
6314 
6315  /* assert( printf("WARNING (BiddyManagedFoaVariable): variable or formula %s already exists\n",x) ); */
6316 
6317  }
6318 
6319  if (isNumbered) {
6320  free(x);
6321  }
6322 
6323  /* DEBUGGING */
6324  /*
6325  printf("GLOBAL ORDERING AFTER FOA: ");
6326  for (w=0; w<biddyVariableTable.num; w++) {
6327  printf("<%s(%u)-%u>",biddyVariableTable.table[w].name,w,getGlobalOrdering(MNG,w));
6328  }
6329  printf("\n");
6330  */
6331 
6332  /* RETURN VARIABLE, WHICH HAS BEEN LOOKED FOR */
6333  return v;
6334 }
6335 
6336 /***************************************************************************/
6345 void
6346 BiddyManagedChangeVariableName(Biddy_Manager MNG, Biddy_Variable v, Biddy_String x)
6347 {
6348  Biddy_Variable min,max,wold,wnew;
6349  Biddy_String tmp;
6350  Biddy_Boolean find;
6351  int cc;
6352 
6353  assert( MNG );
6354 
6355  if (v == 0) return; /* constant variable cannot be renamed */
6356  if (v >= biddyVariableTable.num) return; /* unexisting varible */
6357 
6358  /* FIND THE POSITION OF NEW NAME IN LOOKUP TABLE */
6359  min = 0;
6360  max = biddyVariableTable.num - 1;
6361  find = FALSE;
6362  cc = strcmp(x,biddyVariableTable.lookup[min].name);
6363  if (cc == 0) {
6364  wnew = min;
6365  find = TRUE;
6366  } else if (cc < 0) {
6367  wnew = min;
6368  find = FALSE;
6369  } else {
6370  cc = strcmp(x,biddyVariableTable.lookup[max].name);
6371  if (cc == 0) {
6372  wnew = max;
6373  find = TRUE;
6374  } else if (cc > 0) {
6375  wnew = max+1;
6376  find = FALSE;
6377  } else {
6378  wnew = (min + max) / 2;
6379  while (wnew != min) {
6380  cc = strcmp(x,biddyVariableTable.lookup[wnew].name);
6381  if (cc == 0) {
6382  min = max = wnew;
6383  find = TRUE;
6384  } else if (cc < 0) {
6385  max = wnew;
6386  } else {
6387  min = wnew;
6388  }
6389  wnew = (min + max) / 2;
6390  }
6391  if (!find) wnew++;
6392  }
6393  }
6394 
6395  if (find) {
6396  fprintf(stderr,"(ERROR) BiddyManagedChangeVariableName: new name %s already exists!\n",x);
6397  exit(1);
6398  }
6399 
6400  /* IF NEW NAME LOOKS AS A NUMBER THEN ADAPT numnum TO AVOID PROBLEMS AFTER ADDING NUMBERED VARIABLES */
6401  if (x) {
6402 #ifdef PLAIN
6403  sscanf(x,"%u",&v);
6404 #else
6405  sscanf(x,"%hu",&v);
6406 #endif
6407  tmp = strdup(x);
6408 #ifdef PLAIN
6409  sprintf(tmp,"%u",v);
6410 #else
6411  sprintf(tmp,"%hu",v);
6412 #endif
6413  if (!strcmp(x,tmp)) {
6414  if (biddyVariableTable.numnum < v) biddyVariableTable.numnum = v;
6415  }
6416  free(tmp);
6417  }
6418 
6419  /* FIND OLD NAME IN LOOKUP TABLE */
6420  min = 0;
6421  max = biddyVariableTable.num - 1;
6422  find = FALSE;
6423  cc = strcmp(biddyVariableTable.table[v].name,biddyVariableTable.lookup[min].name);
6424  if (cc == 0) {
6425  wold = min;
6426  find = TRUE;
6427  } else if (cc < 0) {
6428  wold = min;
6429  find = FALSE;
6430  } else {
6431  cc = strcmp(biddyVariableTable.table[v].name,biddyVariableTable.lookup[max].name);
6432  if (cc == 0) {
6433  wold = max;
6434  find = TRUE;
6435  } else if (cc > 0) {
6436  wold = max+1;
6437  find = FALSE;
6438  } else {
6439  wold = (min + max) / 2;
6440  while (wold != min) {
6441  cc = strcmp(biddyVariableTable.table[v].name,biddyVariableTable.lookup[wold].name);
6442  if (cc == 0) {
6443  min = max = wold;
6444  find = TRUE;
6445  } else if (cc < 0) {
6446  max = wold;
6447  } else {
6448  min = wold;
6449  }
6450  wold = (min + max) / 2;
6451  }
6452  if (!find) wold++;
6453  }
6454  }
6455 
6456  assert ( wold < biddyVariableTable.num);
6457 
6458  if (wold < wnew) wnew--;
6459 
6460  /* RENAME */
6461  free(biddyVariableTable.table[v].name);
6462  biddyVariableTable.table[v].name = strdup(x);
6463 
6464  /* REMOVE VARIABLE FROM LOOKUP TABLE */
6465  memmove(&biddyVariableTable.lookup[wold],&biddyVariableTable.lookup[wold+1],(biddyVariableTable.num-wold-1)*sizeof(BiddyLookupVariable));
6466 
6467  /* ADD NEW NAME TO LOOKUP TABLE */
6468  memmove(&biddyVariableTable.lookup[wnew+1],&biddyVariableTable.lookup[wnew],(biddyVariableTable.num-wnew-1)*sizeof(BiddyLookupVariable));
6469  biddyVariableTable.lookup[wnew].name = biddyVariableTable.table[v].name;
6470  biddyVariableTable.lookup[wnew].v = v;
6471 
6472  /* DEBUGGING */
6473  /*
6474  printf("BiddyManagedChangeVariableName %s: biddyVariableTable.num = %u\n",x,biddyVariableTable.num);
6475  printf("BiddyManagedChangeVariableName %s: biddyVariableTable.numnum = %u\n",x,biddyVariableTable.numnum);
6476  */
6477 }
6478 
6479 /***************************************************************************/
6489 BiddyManagedAddVariableByName(Biddy_Manager MNG, Biddy_String x)
6490 {
6491  assert( MNG );
6492 
6493  return BiddyManagedFoaVariable(MNG,x,TRUE,FALSE);
6494 }
6495 
6496 /***************************************************************************/
6506 BiddyManagedAddElementByName(Biddy_Manager MNG, Biddy_String x)
6507 {
6508  assert( MNG );
6509 
6510  return BiddyManagedFoaVariable(MNG,x,FALSE,FALSE);
6511 }
6512 
6513 /***************************************************************************/
6522 Biddy_Edge
6523 BiddyManagedAddVariableBelow(Biddy_Manager MNG, Biddy_Variable v)
6524 {
6525  Biddy_Edge f;
6526  Biddy_Variable x;
6527  Biddy_Variable i;
6528 
6529  assert( MNG );
6530 
6531  assert( v > 0 );
6532  assert( v < biddyVariableTable.num );
6533 
6534  if (v == 0) {
6535  fprintf(stderr,"WARNING: variable cannot be added below constant variable\n");
6536  return biddyNull;
6537  }
6538 
6539  if (v >= biddyVariableTable.num ) {
6540  fprintf(stderr,"WARNING: variable cannot be added below the non-existing node\n");
6541  return biddyNull;
6542  }
6543 
6544  /* only numbered variable will be added, element will not be added */
6545  f = BiddyManagedGetVariableEdge(MNG,BiddyManagedAddVariableByName(MNG,NULL));
6546 
6547  /* FOR OBDDs AND OFDDs, NEW VARIABLE WAS ADDED BELOW OF ALL THE EXISTING ONES */
6548  /* FOR ZBDDs AND ZFDDs, NEW VARIABLE WAS ADDED ABOVE OF ALL THE EXISTING ONES */
6549  /* FOR TZBDDs AND TZFDDs, NEW VARIABLE WAS ADDED ABOVE OF ALL THE EXISTING ONES */
6550 
6551  x = biddyVariableTable.num - 1; /* position in the table, not in the ordering! */
6552 
6553  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
6554  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
6555  {
6556  /* NO NODE WITH NEW VARIABLE EXISTS, YET */
6557  /* (because element has not been created) */
6558  /* THUS, VARIABLE CAN BE SHIFTED WITHOUT IMPACT ON THE REPRESENTED FUNCTIONS/COMBINATION SETS */
6559  if (v == biddyVariableTable.table[0].prev) return f; /* variable ordering is already OK */
6560  biddyVariableTable.table[0].prev = biddyVariableTable.table[x].prev;
6561  biddyVariableTable.table[biddyVariableTable.table[x].prev].next = 0;
6562  biddyVariableTable.table[biddyVariableTable.table[v].next].prev = x;
6563  biddyVariableTable.table[x].next = biddyVariableTable.table[v].next;
6564  biddyVariableTable.table[x].prev = v;
6565  biddyVariableTable.table[v].next = x;
6566 
6567 #ifdef VARIABLEORDERINGMATRIX_YES
6568  for (i=0; i<biddyVariableTable.size; i++) {
6569  if (BiddyIsSmaller(biddyOrderingTable,v,i)) {
6570  SET_ORDER(biddyOrderingTable,x,i);
6571  CLEAR_ORDER(biddyOrderingTable,i,x);
6572  } else {
6573  SET_ORDER(biddyOrderingTable,i,x);
6574  CLEAR_ORDER(biddyOrderingTable,x,i);
6575  }
6576  }
6577 #else
6578  /* THIS WILL SET ORDERING OF NEW VARIABLE TO ordering[v] +1 AND INCREMENT THE ORDERING OF ALL LOWER ONES BY 1 */
6579  /* THIS IS NOT A GENERAL SOLUTION */
6580  /* THE PROBLEM IS IN THE CASE WHERE VALUES OF ordering[] ARE NOT CONSECUTIVE NUMBERS */
6581  biddyOrderingTable[x] = biddyOrderingTable[v] + 1;
6582  for (i=1; i<biddyVariableTable.size-1; i++) {
6583  if (biddyOrderingTable[i] > biddyOrderingTable[v]) {
6584  biddyOrderingTable[i] = biddyOrderingTable[i] + 1;
6585  }
6586  }
6587 #endif
6588  }
6589 #ifndef COMPACT
6590  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
6591  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD))
6592  {
6593  /* NOT IMPLEMENTED, YET */
6594  /* ADDING ELEMENTS COULD BE SUPPORTED IN THE SIMILAR WAY AS ABOVE */
6595  fprintf(stderr,"BiddyManagedAddVariableBelow:: this BDD type is not supported, yet!\n");
6596  return biddyNull;
6597  }
6598  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
6599  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6600  {
6601  /* NOT IMPLEMENTED, YET */
6602  fprintf(stderr,"BiddyManagedAddVariableBelow:: this BDD type is not supported, yet!\n");
6603  return biddyNull;
6604  } else {
6605  fprintf(stderr,"BiddyManagedAddVariableBelow: Unsupported BDD type!\n");
6606  return biddyNull;
6607  }
6608 #endif
6609 
6610  /* *** ADAPTING CACHE TABLES *** */
6611 
6612  /* FOR OBDDs AND OFDDs, NO CACHE TABLES NEED TO BE ADAPTED IN ANY CASE */
6613  /* FOR ZBDDs AND ZFDDs, NO CACHE TABLES NEED TO BE ADAPTED IN ANY CASE */
6614  /* FOR TZBDDs AND TZFDDs, RESULTS IN CACHE TABLES WHERE ONE OF TOP VARIABLE IS ABOVE THE NEW VARIABLE MAY BE WRONG! */
6615  /* AN EXAMPLE FOR TZBDDS: ... */
6616 
6617  /* TESTING AND DEBUGGING */
6618  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
6619  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6620  {
6621  /*
6622  printf("BiddyManagedFoaVariable: variable \"%s\"(%u) added, cleaning cache tables\n",x,v);
6623  */
6624 
6625  /* VARIANT 1: DELETE ONLY INVALID RESULTS */
6626  /*
6627  BiddyOPGarbageNewVariable(MNG,v);
6628  BiddyEAGarbageNewVariable(MNG,v);
6629  BiddyRCGarbageNewVariable(MNG,v);
6630  BiddyReplaceGarbageNewVariable(MNG,v);
6631  */
6632 
6633  /* VARIANT 2: SIMPLY DELETE ALL RESULTS */
6634  /*
6635  BiddyOPGarbageDeleteAll(MNG);
6636  BiddyEAGarbageDeleteAll(MNG);
6637  BiddyRCGarbageDeleteAll(MNG);
6638  BiddyReplaceGarbageDeleteAll(MNG);
6639  */
6640  }
6641 
6642  return f;
6643 }
6644 
6645 /***************************************************************************/
6654 Biddy_Edge
6655 BiddyManagedAddVariableAbove(Biddy_Manager MNG, Biddy_Variable v)
6656 {
6657  Biddy_Edge f;
6658  Biddy_Variable x;
6659  Biddy_Variable i;
6660 
6661  assert( MNG );
6662 
6663  assert( v < biddyVariableTable.num );
6664 
6665  if (v >= biddyVariableTable.num ) {
6666  fprintf(stderr,"WARNING: variable cannot be added above the non-existing node\n");
6667  return biddyNull;
6668  }
6669 
6670  /* only numbered variable will be added, element will not be added */
6671  f = BiddyManagedGetVariableEdge(MNG,BiddyManagedAddVariableByName(MNG,NULL));
6672 
6673  /* FOR OBDDs AND OFDDs, NEW VARIABLE WAS ADDED BELOW OF ALL THE EXISTING ONES */
6674  /* FOR ZBDDs AND ZFDDs, NEW VARIABLE WAS ADDED ABOVE OF ALL THE EXISTING ONES */
6675  /* FOR TZBDDs AND TZFDDs, NEW VARIABLE WAS ADDED ABOVE OF ALL THE EXISTING ONES */
6676 
6677  x = biddyVariableTable.num - 1; /* position in the table, not in the ordering! */
6678 
6679  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
6680  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
6681  {
6682  /* NO NODE WITH NEW VARIABLE EXISTS, YET */
6683  /* (because element has not been created) */
6684  /* THUS, VARIABLE CAN BE SHIFTED WITHOUT IMPACT ON THE REPRESENTED FUNCTIONS/COMBINATION SETS */
6685  if (v == 0) return f; /* variable ordering is already OK */
6686  biddyVariableTable.table[0].prev = biddyVariableTable.table[x].prev;
6687  biddyVariableTable.table[biddyVariableTable.table[x].prev].next = 0;
6688  if (biddyVariableTable.table[v].prev != biddyVariableTable.size) {
6689  biddyVariableTable.table[biddyVariableTable.table[v].prev].next = x;
6690  }
6691  biddyVariableTable.table[x].prev = biddyVariableTable.table[v].prev;
6692  biddyVariableTable.table[x].next = v;
6693  biddyVariableTable.table[v].prev = x;
6694 
6695 #ifdef VARIABLEORDERINGMATRIX_YES
6696  for (i=0; i<biddyVariableTable.size; i++) {
6697  if (BiddyIsSmaller(biddyOrderingTable,i,v)) {
6698  SET_ORDER(biddyOrderingTable,i,x);
6699  CLEAR_ORDER(biddyOrderingTable,x,i);
6700  } else {
6701  SET_ORDER(biddyOrderingTable,x,i);
6702  CLEAR_ORDER(biddyOrderingTable,i,x);
6703  }
6704  }
6705 #else
6706  /* THIS WILL SET ORDERING OF NEW VARIABLE TO ordering[v] AND INCREMENT THE ORDERING OF ALL LOWER ONES BY 1 */
6707  /* THIS IS NOT A GENERAL SOLUTION */
6708  /* THE PROBLEM IS IN THE CASE WHERE VALUES OF ordering[] ARE NOT CONSECUTIVE NUMBERS */
6709  biddyOrderingTable[x] = biddyOrderingTable[v];
6710  for (i=1; i<biddyVariableTable.size-1; i++) {
6711  if (biddyOrderingTable[i] >= biddyOrderingTable[v]) {
6712  biddyOrderingTable[i] = biddyOrderingTable[i] + 1;
6713  }
6714  }
6715 #endif
6716  }
6717 #ifndef COMPACT
6718  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
6719  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD))
6720  {
6721  /* NOT IMPLEMENTED, YET */
6722  /* ADDING ELEMENTS COULD BE SUPPORTED IN THE SIMILAR WAY AS ABOVE */
6723  fprintf(stderr,"BiddyManagedAddVariableAbove: this BDD type is not supported, yet!\n");
6724  return biddyNull;
6725  }
6726  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
6727  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6728  {
6729  /* NOT IMPLEMENTED, YET */
6730  fprintf(stderr,"BiddyManagedAddVariableAbove: this BDD type is not supported, yet!\n");
6731  return biddyNull;
6732  } else {
6733  fprintf(stderr,"BiddyManagedAddVariableAbove: Unsupported BDD type!\n");
6734  return biddyNull;
6735  }
6736 #endif
6737 
6738  /* *** ADAPTING CACHE TABLES *** */
6739 
6740  /* FOR OBDDs AND OFDDs, NO CACHE TABLES NEED TO BE ADAPTED IN ANY CASE */
6741  /* FOR ZBDDs AND ZFDDs, NO CACHE TABLES NEED TO BE ADAPTED IN ANY CASE */
6742  /* FOR TZBDDs AND TZFDDs, RESULTS IN CACHE TABLES WHERE ONE OF TOP VARIABLE IS ABOVE THE NEW VARIABLE MAY BE WRONG! */
6743  /* AN EXAMPLE FOR TZBDDS: ... */
6744 
6745  /* TESTING AND DEBUGGING */
6746  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
6747  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6748  {
6749  /*
6750  printf("BiddyManagedFoaVariable: variable \"%s\"(%u) added, cleaning cache tables\n",x,v);
6751  */
6752 
6753  /* VARIANT 1: DELETE ONLY INVALID RESULTS */
6754  /*
6755  BiddyOPGarbageNewVariable(MNG,v);
6756  BiddyEAGarbageNewVariable(MNG,v);
6757  BiddyRCGarbageNewVariable(MNG,v);
6758  BiddyReplaceGarbageNewVariable(MNG,v);
6759  */
6760 
6761  /* VARIANT 2: SIMPLY DELETE ALL RESULTS */
6762  /*
6763  BiddyOPGarbageDeleteAll(MNG);
6764  BiddyEAGarbageDeleteAll(MNG);
6765  BiddyRCGarbageDeleteAll(MNG);
6766  BiddyReplaceGarbageDeleteAll(MNG);
6767  */
6768  }
6769 
6770  return f;
6771 }
6772 
6773 /***************************************************************************/
6782 Biddy_Edge
6783 BiddyManagedIncTag(Biddy_Manager MNG, Biddy_Edge f)
6784 {
6785 #ifndef COMPACT
6786  Biddy_Variable tag,var;
6787 #endif
6788 
6789  assert( MNG );
6790 
6791  assert(
6792  (biddyManagerType == BIDDYTYPETZBDD) ||
6793  (biddyManagerType == BIDDYTYPETZBDDC) ||
6794  (biddyManagerType == BIDDYTYPETZFDD) ||
6795  (biddyManagerType == BIDDYTYPETZFDDC)
6796  );
6797 
6798 #ifndef COMPACT
6799  tag = BiddyGetTag(f);
6800  var = BiddyV(f);
6801 
6802  assert( BiddyIsSmaller(biddyOrderingTable,tag,var) );
6803 
6804  tag = biddyVariableTable.table[tag].next;
6805 
6806  if (biddyManagerType == BIDDYTYPETZBDD) {
6807 
6808  /* WE HAVE TO CHECK IF MINIMIZATION RULE 3 CAN BE APPLIED */
6809  if (var && (var == tag) && (BiddyE(f) == BiddyT(f))) {
6810  f = BiddyE(f);
6811  } else {
6812  BiddySetTag(f,tag);
6813  }
6814 
6815  assert ( (BiddyGetTag(f) == BiddyV(f)) || BiddyIsSmaller(biddyOrderingTable,BiddyGetTag(f),BiddyV(f)) );
6816 
6817  } else if (biddyManagerType == BIDDYTYPETZBDDC) {
6818  /* TO DO: NOT IMPLEMENTED, YET */
6819  }
6820 #endif
6821 
6822  return f;
6823 }
6824 
6825 /***************************************************************************/
6834 Biddy_Edge
6835 BiddyManagedTaggedFoaNode(Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge pf,
6836  Biddy_Edge pt, Biddy_Variable ptag,
6837  Biddy_Boolean garbageAllowed)
6838 {
6839  unsigned int hash;
6840  Biddy_Edge edge;
6841  BiddyNode *sup, *sup1;
6842  Biddy_Boolean complementedResult;
6843  unsigned int i;
6844  BiddyNode ** tmp;
6845  Biddy_Boolean addNodeSpecial;
6846 #ifndef COMPACT
6847  Biddy_Variable tag;
6848 #endif
6849 
6850  static BiddyNode *newFreeNodes;
6851 
6852  /* DEBUGGING */
6853  /*
6854  printf("BiddyManagedTaggedFoaNode: %p, %d\n",MNG,BiddyManagedGetManagerType(MNG));
6855  */
6856 
6857  assert( MNG );
6858 
6859  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
6860  assert(
6861  (biddyManagerType == BIDDYTYPEOBDD) ||
6862  (biddyManagerType == BIDDYTYPEOBDDC) ||
6863  (biddyManagerType == BIDDYTYPEZBDD) ||
6864  (biddyManagerType == BIDDYTYPEZBDDC) ||
6865  (biddyManagerType == BIDDYTYPETZBDD)
6866  );
6867 
6868  assert( v != 0 );
6869 
6870  /* CURRENTLY, SPECIAL CASE 2 IS ONLY INTENDED FOR USE WITH TAGGED BDDs */
6871  /* TO DO: USE SPECIAL CASE 2 FOR ALL BDD TYPES TO IMPROVE GRAPH COPYING/CONSTRUCTING */
6872  assert( (biddyManagerType == BIDDYTYPETZBDD) ||
6873  (biddyManagerType == BIDDYTYPETZBDDC) ||
6874  (ptag != 0) );
6875 
6876 #ifdef BIDDYEXTENDEDSTATS_YES
6877  biddyNodeTable.foa++;
6878 #endif
6879 
6880  /* DEBUGGING */
6881  /*
6882  printf("FOANODE: v=%u, pf = %p, pt = %p, tag = %u, biddyNull = %p\n",v,pf,pt,biddyNull,NULL);
6883  */
6884 
6885  /* DISABLE GC */
6886  /*
6887  garbageAllowed = FALSE;
6888  */
6889 
6890  addNodeSpecial = FALSE;
6891  complementedResult = FALSE;
6892 
6893  /* SPECIAL CASE 1: pf == pt == NULL */
6894 
6895  if (!pf) {
6896  assert( !pt );
6897  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
6898  pf = biddyZero;
6899  pt = biddyTerminal;
6900  }
6901 #ifndef COMPACT
6902  else if (biddyManagerType == BIDDYTYPEZBDD) {
6903  pf = biddyZero;
6904  pt = biddyTerminal;
6905  }
6906  else if (biddyManagerType == BIDDYTYPEZBDDC) {
6907  pf = biddyTerminal;
6908  pt = biddyTerminal;
6909  complementedResult = TRUE;
6910  }
6911  else if (biddyManagerType == BIDDYTYPETZBDD) {
6912  pf = biddyZero;
6913  pt = biddyTerminal;
6914  }
6915  else if (biddyManagerType == BIDDYTYPETZBDDC) {
6916  pf = biddyTerminal;
6917  pt = biddyTerminal;
6918  complementedResult = TRUE;
6919  }
6920 #endif
6921  ptag = v;
6922  addNodeSpecial = TRUE;
6923  } else {
6924 
6925  /* DEBUGGING */
6926  /*
6927  printf("FOANODE NOT SPECIAL CASE 1 (%d)",BiddyManagedGetManagerType(MNG));
6928  if (addNodeSpecial) {
6929  printf("(addNodeSpecial==TRUE)");
6930  }
6931  printf(": v = <%s>%s, pf = <%s>%s, pt = <%s>%s\n",
6932  biddyVariableTable.table[ptag].name,
6933  biddyVariableTable.table[v].name,
6934  biddyVariableTable.table[BiddyGetTag(pf)].name,
6935  BiddyGetMark(pf)?"0":BiddyManagedGetTopVariableName(MNG,pf),
6936  biddyVariableTable.table[BiddyGetTag(pt)].name,
6937  BiddyGetMark(pt)?"0":BiddyManagedGetTopVariableName(MNG,pt));
6938  */
6939 
6940  assert( BiddyIsSmaller(biddyOrderingTable,v,BiddyV(pf)) );
6941  assert( BiddyIsSmaller(biddyOrderingTable,v,BiddyV(pt)) );
6942  }
6943 
6944  /* DEBUGGING */
6945  /*
6946  printf("FOANODE AFTER CHECKING SPECIAL CASE 1 (%d)",BiddyManagedGetManagerType(MNG));
6947  if (addNodeSpecial) {
6948  printf("(addNodeSpecial==TRUE)");
6949  }
6950  printf(": v = <%s>%s, pf = <%s>%s, pt = <%s>%s\n",
6951  biddyVariableTable.table[ptag].name,
6952  biddyVariableTable.table[v].name,
6953  biddyVariableTable.table[BiddyGetTag(pf)].name,
6954  BiddyGetMark(pf)?"0":BiddyManagedGetTopVariableName(MNG,pf),
6955  biddyVariableTable.table[BiddyGetTag(pt)].name,
6956  BiddyGetMark(pt)?"0":BiddyManagedGetTopVariableName(MNG,pt));
6957  */
6958 
6959  /* SPECIAL CASE 2: ptag == 0 */
6960 
6961  /* the reduction rule and the normalization of complemented edges is not used */
6962  /* the node is added exactly as specified (be careful, this may create a wrong node!) */
6963 
6964  /* NORMAL CASE ptag != 0 */
6965 
6966  if (!addNodeSpecial && ptag) {
6967 
6968  /* SIMPLE CASES */
6969 
6970  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
6971  if (pf == pt) {
6972  return pf;
6973  }
6974  }
6975 
6976 #ifndef COMPACT
6977  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
6978  if (pt == biddyZero) {
6979  return pf;
6980  }
6981  }
6982 
6983  else if (biddyManagerType == BIDDYTYPETZBDD) {
6984  if (BiddyR(pt) == biddyZero) {
6985  if (BiddyR(pf) == biddyZero) {
6986  return biddyZero;
6987  }
6988  tag = BiddyGetTag(pf);
6989  v = biddyVariableTable.table[v].next;
6990  if (tag == v) {
6991  return BiddySetTag(pf,ptag);
6992  } else {
6993  return BiddyManagedTaggedFoaNode(MNG,v,pf,pf,ptag,garbageAllowed);
6994  }
6995  }
6996  if (pf == pt) {
6997  if (ptag == v) {
6998  return pf;
6999  }
7000  }
7001  }
7002 #endif
7003 
7004  /* NORMALIZATION OF COMPLEMENTED EDGES */
7005 
7006  if (biddyManagerType == BIDDYTYPEOBDDC) {
7007  if (BiddyGetMark(pt)) {
7008  BiddyInvertMark(pf);
7009  BiddyClearMark(pt);
7010  complementedResult = TRUE;
7011  } else {
7012  complementedResult = FALSE;
7013  }
7014  }
7015 
7016 #ifndef COMPACT
7017  else if (biddyManagerType == BIDDYTYPEZBDDC) {
7018  if (BiddyGetMark(pf)) {
7019  BiddyClearMark(pf);
7020  complementedResult = TRUE;
7021  } else {
7022  complementedResult = FALSE;
7023  }
7024  }
7025 
7026  else if (biddyManagerType == BIDDYTYPETZBDD) {
7027  /* COMPLEMENTED EDGES ARE NOT USED */
7028  }
7029 #endif
7030 
7031  }
7032 
7033  /* SOME NODES ARE NOT HASHED IN THE USUAL WAY */
7034  /* FOR THEM, THE RESULTING EDGE IS STORED ONLY AS PART OF BiddyVariable */
7035  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
7036  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
7037  {
7038  if ((pf == biddyZero) && (pt == biddyTerminal) && !addNodeSpecial) {
7039  if (complementedResult) {
7040  return BiddyInv(biddyVariableTable.table[v].variable);
7041  } else {
7042  return biddyVariableTable.table[v].variable;
7043  }
7044  }
7045  }
7046 #ifndef COMPACT
7047  else if ((biddyManagerType == BIDDYTYPEZBDD) || (biddyManagerType == BIDDYTYPEZFDD))
7048  {
7049  if ((pf == biddyZero) && (pt == biddyTerminal) && !addNodeSpecial) {
7050  return biddyVariableTable.table[v].element;
7051  }
7052  }
7053  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZFDDC))
7054  {
7055  if ((pf == biddyTerminal) && (pt == biddyTerminal) && !addNodeSpecial) {
7056  if (complementedResult) {
7057  return biddyVariableTable.table[v].element;
7058  }
7059  else {
7060  return BiddyInv(biddyVariableTable.table[v].element);
7061  }
7062  }
7063  }
7064  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
7065  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
7066  {
7067  if ((pf == biddyZero) && (pt == biddyTerminal) && !addNodeSpecial) {
7068  edge = biddyVariableTable.table[v].variable;
7069  BiddySetTag(edge,ptag);
7070  return edge;
7071  }
7072  }
7073 #endif
7074 
7075  /* FIND OR ADD - THERE IS A HASH TABLE WITH CHAINING */
7076  /* THE CREATED NODE WILL ALWAYS BE THE FIRST NODE IN THE CHAIN */
7077  /* BECAUSE OF USED TRICKS, HASH FUNCTION MUST NEVER RETURN ZERO! */
7078  /* VARIABLES/ELEMENTS (v,0,1) ARE NOT HASHED IN THE USUAL WAY */
7079 
7080  if (addNodeSpecial) {
7081  sup = sup1 = NULL;
7082  hash = 0;
7083  } else {
7084  hash = nodeTableHash(v,pf,pt,biddyNodeTable.size);
7085  sup = biddyNodeTable.table[hash];
7086  sup1 = findNodeTable(MNG,v,pf,pt,&sup);
7087  }
7088 
7089  if ((!sup) || (v != sup->v)) {
7090 
7091  /* NEW NODE MUST BE ADDED */
7092 
7093  /* IF ALL GENERATED NODES ARE USED THEN TRY GARBAGE COLLECTION */
7094  if (garbageAllowed && !biddyFreeNodes) {
7095 
7096  /* PROFILING */
7097  /*
7098  fprintf(stderr,"AutoGC IN: biddyNodeTable.num = %u, biddyNodeTable.generated = %u\n",biddyNodeTable.num,biddyNodeTable.generated);
7099  */
7100 
7101  BiddyManagedAutoGC(MNG);
7102 
7103  /* PROFILING */
7104  /*
7105  fprintf(stderr,"AutoGC OUT: biddyNodeTable.num = %u, biddyNodeTable.generated = %u, free = %u (%.2f)\n",
7106  biddyNodeTable.num,biddyNodeTable.generated,biddyNodeTable.generated-biddyNodeTable.num,100.0*biddyNodeTable.num/biddyNodeTable.generated);
7107  */
7108 
7109  /* the table may be resized, thus the element must be rehashed */
7110  hash = nodeTableHash(v, pf, pt, biddyNodeTable.size);
7111  sup = biddyNodeTable.table[hash];
7112  sup1 = findNodeTable(MNG, v, pf, pt, &sup);
7113 
7114  }
7115 
7116  /* IF NO FREE NODES ARE FOUND THEN CREATE NEW BLOCK OF NODES */
7117  if (!biddyFreeNodes) {
7118 
7119  /* the size of a memory block is increased until the limit is reached */
7120  if (biddyNodeTable.blocksize < biddyNodeTable.limitblocksize)
7121  {
7122  biddyNodeTable.blocksize = biddyNodeTable.resizeratio * biddyNodeTable.size;
7123  if (biddyNodeTable.blocksize < biddyNodeTable.initblocksize)
7124  biddyNodeTable.blocksize = biddyNodeTable.initblocksize;
7125  if (biddyNodeTable.blocksize > biddyNodeTable.limitblocksize)
7126  biddyNodeTable.blocksize = biddyNodeTable.limitblocksize;
7127 
7128  /* PROFILING */
7129  /*
7130  printf(">");
7131  */
7132  }
7133 
7134  /* PROFILING */
7135  /*
7136  else {
7137  printf("=");
7138  }
7139  */
7140 
7141  if (!(newFreeNodes = (BiddyNode *)
7142  malloc((biddyNodeTable.blocksize) * sizeof(BiddyNode))))
7143  {
7144  fprintf(stderr, "\nBIDDY (BiddyManagedTaggedFoaNode): Out of memory error!\n");
7145  fprintf(stderr, "Currently, there exist %d nodes.\n", biddyNodeTable.num);
7146  exit(1);
7147  }
7148 
7149  biddyNodeTable.blocknumber++;
7150  if (!(tmp = (BiddyNode **)realloc(biddyNodeTable.blocktable,
7151  biddyNodeTable.blocknumber * sizeof(BiddyNode *))))
7152  {
7153  fprintf(stderr, "\nBIDDY (BiddyManagedTaggedFoaNode): Out of memory error!\n");
7154  fprintf(stderr, "Currently, there exist %d nodes.\n", biddyNodeTable.num);
7155  exit(1);
7156  }
7157  biddyNodeTable.blocktable = tmp;
7158  biddyNodeTable.blocktable[biddyNodeTable.blocknumber - 1] = newFreeNodes;
7159  biddyNodeTable.generated = biddyNodeTable.generated + biddyNodeTable.blocksize;
7160 
7161  newFreeNodes[biddyNodeTable.blocksize - 1].list = biddyFreeNodes;
7162  biddyFreeNodes = newFreeNodes;
7163  for (i = 0; i < biddyNodeTable.blocksize - 1; i++) {
7164  newFreeNodes = (BiddyNode*)(newFreeNodes->list = &newFreeNodes[1]);
7165  }
7166 
7167  /* PROFILING */
7168  /*
7169  fprintf(stderr,"FOANODE NEW BLOCK: biddyNodeTable.num = %u, biddyNodeTable.generated = %u, free = %u (%.2f)\n",
7170  biddyNodeTable.num,biddyNodeTable.generated,biddyNodeTable.generated-biddyNodeTable.num,100.0*biddyNodeTable.num/biddyNodeTable.generated);
7171  */
7172 
7173  }
7174 
7175  /* ADDING NEW NODE */
7176  (biddyNodeTable.num)++;
7177  if (biddyNodeTable.num > biddyNodeTable.max) biddyNodeTable.max = biddyNodeTable.num;
7178  (biddyVariableTable.table[v].num)++;
7179 
7180  sup = biddyFreeNodes;
7181  biddyFreeNodes = (BiddyNode *)sup->list;
7182 
7183  /* DEBUGGING */
7184  /*
7185  printf("FOANODE after the normalization: (%s,%s,%s)\n",
7186  BiddyManagedGetVariableName(MNG,v),
7187  BiddyManagedGetVariableName(MNG,BiddyV(pf)),
7188  BiddyManagedGetVariableName(MNG,BiddyV(pt))
7189  );
7190  */
7191 
7192  assert(BiddyIsSmaller(biddyOrderingTable,v,BiddyV(pf)));
7193  assert(BiddyIsSmaller(biddyOrderingTable,v,BiddyV(pt)));
7194 
7195  sup->f = pf; /* BE CAREFULL !!!! */
7196  sup->t = pt; /* you can create node with an arbitrary (wrong!) ordering */
7197  if (addNodeSpecial) {
7198  sup->expiry = biddySystemAge; /* variable/element node is refreshed! */
7199  } else {
7200  sup->expiry = 1; /* other nodes are not refreshed! */
7201  }
7202  sup->select = 0;
7203  sup->v = v;
7204 
7205  /* add new node to Node table */
7206  /* nodes (v,0,1) are not stored in Node table */
7207  if (!addNodeSpecial) {
7208  addNodeTable(MNG, hash, sup, sup1);
7209  }
7210 
7211  /* add new node to the list */
7212  /* all nodes are added to list, also variables/elements which are not added to Node table */
7213  /* lastNode->list IS NOT FIXED! */
7214  /* YOU MUST NEVER ASSUME THAT lastNode->list = NULL */
7215  biddyVariableTable.table[v].lastNode->list = (void *)sup;
7216  biddyVariableTable.table[v].lastNode = sup;
7217 
7218  }
7219 
7220  edge = sup;
7221 
7222  if (complementedResult) {
7223  BiddySetMark(edge);
7224  }
7225 
7226  if ((biddyManagerType == BIDDYTYPETZBDD) && ptag) {
7227  BiddySetTag(edge,ptag);
7228  }
7229 
7230  /* (Biddy v1.5) To enable efficient memory management (e.g. sifting) */
7231  /* the function started with the returned node is not recursively refreshed! */
7232 
7233  /* DEBUGGING */
7234  /*
7235  printf("FOANODE COMPLETE ");
7236  if (addNodeSpecial) printf("(addNodeSpecial==TRUE) ");
7237  debugEdge(MNG,edge);
7238  printf("\n");
7239  */
7240 
7241  /* DEBUGGING */
7242  /*
7243  if (!((biddyManagerType != BIDDYTYPETZBDD) || (BiddyGetTag(edge) == BiddyV(edge)) || BiddyIsSmaller(biddyOrderingTable,BiddyGetTag(edge),BiddyV(edge))))
7244  {
7245  printf("FOANODE ERROR");
7246  if (addNodeSpecial) printf(" (addNodeSpecial==TRUE)");
7247  printf("!\n");
7248  writeORDER(MNG);
7249  debugEdge(MNG,edge);
7250  printf("\n");
7251  }
7252  */
7253 
7254  assert( BiddyIsSmaller(biddyOrderingTable,BiddyV(edge),BiddyV(BiddyE(edge))) );
7255  assert( BiddyIsSmaller(biddyOrderingTable,BiddyV(edge),BiddyV(BiddyT(edge))) );
7256  assert( (biddyManagerType != BIDDYTYPETZBDD) || !ptag || (BiddyGetTag(edge) == BiddyV(edge)) || BiddyIsSmaller(biddyOrderingTable,BiddyGetTag(edge),BiddyV(edge)) );
7257  assert( (biddyManagerType != BIDDYTYPETZBDD) || !ptag || (BiddyGetTag(BiddyE(edge)) == BiddyV(BiddyE(edge))) || BiddyIsSmaller(biddyOrderingTable,BiddyGetTag(BiddyE(edge)),BiddyV(BiddyE(edge))) );
7258  assert( (biddyManagerType != BIDDYTYPETZBDD) || !ptag || (BiddyGetTag(BiddyT(edge)) == BiddyV(BiddyT(edge))) || BiddyIsSmaller(biddyOrderingTable,BiddyGetTag(BiddyT(edge)),BiddyV(BiddyT(edge))) );
7259 
7260  return edge;
7261 }
7262 
7263 /***************************************************************************/
7272 void
7273 BiddyManagedGC(Biddy_Manager MNG, Biddy_Variable targetLT,
7274  Biddy_Variable targetGEQ,Biddy_Boolean purge,
7275  Biddy_Boolean total)
7276 {
7277  unsigned int i,j;
7278  BiddyFormula *tmp;
7279  BiddyNode *tmpnode1,*tmpnode2;
7280  BiddyNode *sup;
7281  BiddyCacheList *c;
7282  Biddy_Boolean cacheOK;
7283  Biddy_Boolean resizeRequired;
7284  Biddy_Boolean gcUseful;
7285  Biddy_Variable v;
7286  unsigned int hash;
7287  clock_t starttime;
7288 
7289  assert( MNG );
7290 
7291  /* DEBUGGING */
7292  /*
7293  {
7294  static int n = 0;
7295  fprintf(stdout,"\nGarbage (%d), targetLT=%u, targetGEQ=%u, systemAge=%u, there are %u BDD nodes, NodeTableSize=%u\n",
7296  ++n,targetLT,targetGEQ,biddySystemAge,biddyNodeTable.num,biddyNodeTable.size);
7297  }
7298  */
7299 
7300  assert( (targetLT == 0) || (targetGEQ != 0) );
7301 
7302  /* PROFILING */
7303  /*
7304  assert( biddyNodeTable.num < 2000000 );
7305  */
7306 
7307  /* GC calls used during sifting are not counted */
7308  if (targetLT == 0) {
7309  biddyNodeTable.garbage++;
7310  }
7311 
7312 #ifdef BIDDYEXTENDEDSTATS_YES
7313  if (!(biddyNodeTable.gcobsolete = (unsigned long long int *) realloc(biddyNodeTable.gcobsolete,
7314  biddyNodeTable.garbage * sizeof(unsigned long long int))))
7315  {
7316  fprintf(stderr,"BiddyManagedGC: Out of memoy!\n");
7317  exit(1);
7318  }
7319  biddyNodeTable.gcobsolete[biddyNodeTable.garbage-1] = 0;
7320 #endif
7321 
7322  /* DEBUGGING - REPORT ALL NODES WITH A SPECIFIC VARIABLE */
7323  /*
7324  {
7325  BiddyNode *sup;
7326  biddyVariableTable.table[3].lastNode->list = NULL;
7327  sup = biddyVariableTable.table[3].firstNode;
7328  while (sup) {
7329  debugNode(MNG,sup);
7330  sup = (BiddyNode *) sup->list;
7331  }
7332  printf("\n");
7333  }
7334  */
7335 
7336  starttime = clock();
7337 
7338  /* REMOVE ALL FORMULAE WHICH ARE NOT PRESERVED ANYMORE */
7339  /* the first two formulae ("0" and "1") are never removed */
7340  /* iff parameter purge is true then all formulae without name are removed */
7341  /* iff parameter purge is true then all deleted formulae (even if fortified/preserved) are removed */
7342  /* iff parameter purge is true then fresh formulae are not removed */
7343 
7344  if (targetLT == 0) {
7345  i = 2;
7346  biddyFormulaTable.numOrdered = 2;
7347  } else {
7348  /* if (targetLT != 0) then there should not obsolete formulae */
7349  i = biddyFormulaTable.size;
7350  }
7351  for (j = i; j < biddyFormulaTable.size; j++) {
7352 
7353  /* DEBUGGING */
7354  /*
7355  printf("[FORM:%s@%u]",biddyFormulaTable.table[j].name,biddyFormulaTable.table[j].expiry);
7356  */
7357 
7358  if (purge && !biddyFormulaTable.table[j].name) {
7359  biddyFormulaTable.table[j].deleted = TRUE;
7360  }
7361 
7362  /* this will not delete fresh formulae */
7363  if ((!purge || !biddyFormulaTable.table[j].deleted)
7364  &&
7365  (!biddyFormulaTable.table[j].expiry || biddyFormulaTable.table[j].expiry >= biddySystemAge))
7366  {
7367 
7368  /* THIS FORMULA IS OK */
7369  if (i != j) {
7370  biddyFormulaTable.table[i] = biddyFormulaTable.table[j];
7371  }
7372  if (biddyFormulaTable.table[i].name) biddyFormulaTable.numOrdered++;
7373  i++;
7374 
7375  } else {
7376 
7377  /* THIS FORMULA IS BAD */
7378 
7379  /* DEBUGGING */
7380  /*
7381  fprintf(stderr,"BiddyManagedGC: Formula %s will be deleted!\n",biddyFormulaTable.table[j].name);
7382  if (biddyFormulaTable.table[j].deleted) fprintf(stderr,"BiddyManagedGC: Formula has DELETED flag!\n");
7383  if (biddyFormulaTable.table[j].expiry && biddyFormulaTable.table[j].expiry < biddySystemAge)
7384  fprintf(stderr,"BiddyManagedGC: Formula is obsolete!\n");
7385  */
7386 
7387  if (biddyFormulaTable.table[j].name) free(biddyFormulaTable.table[j].name);
7388 
7389  }
7390  }
7391 
7392  /* UPDATE FORMULA TABLE */
7393  if (i != biddyFormulaTable.size) {
7394  biddyFormulaTable.size = i;
7395  if (!(tmp = (BiddyFormula *)
7396  realloc(biddyFormulaTable.table,biddyFormulaTable.size*sizeof(BiddyFormula))))
7397  {
7398  fprintf(stderr,"BiddyManagedGC: Out of memoy!\n");
7399  exit(1);
7400  }
7401  biddyFormulaTable.table = tmp;
7402  }
7403 
7404  /* if parameter purge is true then nodes which are not part of any non-obsolete */
7405  /* non-deleted formulae are removed even if they are fresh or fortified */
7406  /* (this should not be used during the automatic garbage collection!) */
7407 
7408  if ((targetLT == 0) && purge) {
7409  for (v=1; v<biddyVariableTable.num; v++) {
7410  biddyVariableTable.table[v].lastNode->list = NULL;
7411  sup = biddyVariableTable.table[v].firstNode;
7412  while (sup) {
7413  sup->expiry = 1;
7414  sup = (BiddyNode *) sup->list;
7415  }
7416  }
7417  }
7418 
7419  /* RESTORE expiry VALUE FOR TOP NODE OF ALL CONSTANTS, VARIABLES, ELEMENTS, AND EXTERNAL FORMULAE */
7420  /* deleted formula have been already removed */
7421  /* THIS IS NEEDED EVEN IF PURGE == FALSE (E.G. SIFTING) */
7422  /* first formula is 0, it is always a single terminal node */
7423  /* second formula is 1, it could be a large graph, e.g. for ZBDD */
7424  BiddyRefresh(biddyZero);
7425  BiddyRefresh(biddyOne);
7426  for (v = 1; v < biddyVariableTable.num; v++) {
7427  if (biddyVariableTable.table[v].variable) BiddyRefresh(biddyVariableTable.table[v].variable);
7428  if (biddyVariableTable.table[v].element) BiddyRefresh(biddyVariableTable.table[v].element);
7429  }
7430  for (j = 1; j < biddyFormulaTable.size; j++) {
7431  if (!BiddyIsNull(biddyFormulaTable.table[j].f) &&
7432  !BiddyIsTerminal(biddyFormulaTable.table[j].f)
7433  )
7434  {
7435  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
7436  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
7437  {
7438  /* VARIANT A: consider variables already refreshed */
7439  /*
7440  if ((BiddyE(biddyFormulaTable.table[j].f) == biddyZero) && (BiddyT(biddyFormulaTable.table[j].f) == biddyTerminal)) {
7441  } else {
7442  BiddyProlongOne(biddyFormulaTable.table[j].f,biddyFormulaTable.table[j].expiry);
7443  }
7444  */
7445  /* VARIANT B: simply prolong all formulae */
7446 
7447  BiddyProlongOne(biddyFormulaTable.table[j].f,biddyFormulaTable.table[j].expiry);
7448 
7449  }
7450 #ifndef COMPACT
7451  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
7452  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD))
7453  {
7454  /* VARIANT A: consider elements already refreshed */
7455  /*
7456  if ((BiddyE(biddyFormulaTable.table[j].f) == biddyTerminal) && (BiddyT(biddyFormulaTable.table[j].f) == biddyTerminal)) {
7457  } else {
7458  BiddyProlongOne(biddyFormulaTable.table[j].f,biddyFormulaTable.table[j].expiry);
7459  }
7460  */
7461  /* VARIANT B: simply prolong all formulae */
7462 
7463  BiddyProlongOne(biddyFormulaTable.table[j].f,biddyFormulaTable.table[j].expiry);
7464 
7465  }
7466  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
7467  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
7468  {
7469  /* VARIANT A: consider variables/elements already refreshed */
7470  /*
7471  if ((BiddyE(biddyFormulaTable.table[j].f) == biddyZero) && (BiddyT(biddyFormulaTable.table[j].f) == biddyTerminal)) {
7472  } else {
7473  BiddyProlongOne(biddyFormulaTable.table[j].f,biddyFormulaTable.table[j].expiry);
7474  }
7475  */
7476  /* VARIANT B: simply prolong all formulae */
7477 
7478  BiddyProlongOne(biddyFormulaTable.table[j].f,biddyFormulaTable.table[j].expiry);
7479 
7480  }
7481 #endif
7482  }
7483  }
7484 
7485  /* REFRESH OBSOLETE NODES WHICH SHOULD NOT BE OBSOLETE */
7486  /* ALSO, COUNT HOW MANY OBSOLETE NODES PER VARIABLE EXIST */
7487  for (v=1; v<biddyVariableTable.num; v++) {
7488  biddyVariableTable.table[v].lastNode->list = NULL;
7489  biddyVariableTable.table[v].numobsolete = 0;
7490  }
7491  for (v=1; v<biddyVariableTable.num; v++) {
7492  /* if (targetLT != 0) then nodes equal or higher (bottom-more) than targetLT */
7493  /* and smaller (top-more) than targetGEQ will not be prolonged */
7494  if (v == targetLT) {
7495  /* there is always at least one node in the list */
7496  sup = biddyVariableTable.table[v].firstNode;
7497  assert( sup != NULL );
7498  while (sup) {
7499  assert(sup->v == v) ;
7500  if ((sup->expiry) && (sup->expiry < biddySystemAge)) {
7501  (biddyVariableTable.table[v].numobsolete)++;
7502  }
7503  sup = (BiddyNode *) sup->list;
7504  }
7505  }
7506  else if ((targetLT == 0) || (BiddyIsSmaller(biddyOrderingTable,v,targetLT))) {
7507  /* (targetLT == 0) used in the above 'if' for the speed, only, all v are smaller (topmore) than variable 0 */
7508  /* there is always at least one node in the list */
7509  sup = biddyVariableTable.table[v].firstNode;
7510  assert( sup != NULL );
7511  assert( sup->v == v );
7512  /* successors of the first node in the list does not need to be prolonged */
7513  sup = (BiddyNode *) sup->list;
7514  while (sup) {
7515  assert( sup->v == v );
7516  if (!(sup->expiry) || (sup->expiry >= biddySystemAge)) {
7517  assert( !BiddyIsNull(BiddyE(sup)) );
7518  assert( !BiddyIsNull(BiddyT(sup)) );
7519  BiddyProlongRecursively(MNG,BiddyE(sup),sup->expiry,targetLT);
7520  BiddyProlongRecursively(MNG,BiddyT(sup),sup->expiry,targetLT);
7521  } else {
7522  (biddyVariableTable.table[v].numobsolete)++;
7523  }
7524  sup = (BiddyNode *) sup->list;
7525  }
7526  }
7527  }
7528 
7529  /* CHECK IF THE RESIZING OF NODE TABLE IS NECESSARY */
7530  i = biddyNodeTable.num; /* we will count how many nodes are non-obsolete */
7531  resizeRequired = FALSE;
7532  for (v=1; v<biddyVariableTable.num; v++) {
7533 
7534  /* there should be at least one non-obsolete node for each variable */
7535  assert ( biddyVariableTable.table[v].numobsolete < biddyVariableTable.table[v].num );
7536 
7537  i = i - biddyVariableTable.table[v].numobsolete;
7538  }
7539  resizeRequired = (
7540  (biddyNodeTable.size < biddyNodeTable.limitsize) &&
7541  (i > biddyNodeTable.resizeratio * biddyNodeTable.size)
7542  );
7543 
7544  /* IF (targetLT != 0) THEN NODE TABLE RESIZING IS DISABLED */
7545  if (targetLT != 0) resizeRequired = FALSE;
7546 
7547  /* CHECK IF THE DELETION OF NODES IS USEFUL - how many nodes will be deleted */
7548  gcUseful = ((biddyNodeTable.num - i) > (biddyNodeTable.gcratio * biddyNodeTable.blocksize));
7549  if (gcUseful) resizeRequired = FALSE;
7550 
7551  /* IF total AND THERE IS SOMETHING TO DELETE THEN gcUseful must be TRUE */
7552  if (total && (i < biddyNodeTable.num)) gcUseful = TRUE;
7553 
7554  /* DEBUGGING */
7555  /*
7556  printf("GC CHECK: %u obsolete nodes ",biddyNodeTable.num - i);
7557  if (gcUseful) printf("(GC useful) "); else printf("(GC NOT useful) ");
7558  if (resizeRequired) printf("(Resize required)"); else printf("Resize NOT required)");
7559  printf("\n");
7560  */
7561 
7562  /* REMOVE ALL OBSOLETE NODES */
7563  cacheOK = TRUE;
7564  if (gcUseful || resizeRequired) {
7565 
7566 #ifdef BIDDYEXTENDEDSTATS_YES
7567  biddyNodeTable.gcobsolete[biddyNodeTable.garbage-1] = (biddyNodeTable.num - i);
7568 #endif
7569 
7570  /* RESIZE NODE TABLE BECASUE IT SEEMS TO BE TO SMALL */
7571  if (resizeRequired) {
7572 
7573  /* DEBUGGING */
7574  /*
7575  printf("BiddyManagedGC: resizeRequired == TRUE\n");
7576  */
7577 
7578  /* REMOVE OLD NODE TABLE */
7579  free(biddyNodeTable.table);
7580  biddyNodeTable.nodetableresize++;
7581 
7582  /* DETERMINE NEW SIZE OF THE NODE TABLE AND ADAPT NODE TABLE PARAMETERS */
7583  while (resizeRequired) {
7584  biddyNodeTable.size = 2 * biddyNodeTable.size + 1;
7585  biddyNodeTable.gcratio = (1.0 - biddyNodeTable.gcratioX) + (biddyNodeTable.gcratio / biddyNodeTable.gcratioF);
7586  biddyNodeTable.resizeratio = (1.0 - biddyNodeTable.resizeratioX) + (biddyNodeTable.resizeratio * biddyNodeTable.resizeratioF);
7587  if (biddyNodeTable.gcratio < 0.0) biddyNodeTable.gcratio = 0.0;
7588  if (biddyNodeTable.resizeratio < 0.0) biddyNodeTable.resizeratio = 0.0;
7589  resizeRequired = (
7590  (biddyNodeTable.size < biddyNodeTable.limitsize) &&
7591  (i > biddyNodeTable.resizeratio * biddyNodeTable.size)
7592  );
7593  }
7594  resizeRequired = TRUE; /* reset variable resizeRequired */
7595 
7596  /* CREATE NEW NODE TABLE */
7597  if (!(biddyNodeTable.table = (BiddyNode **)
7598  calloc((biddyNodeTable.size+2),sizeof(BiddyNode *)))) {
7599  fprintf(stderr,"BiddyManagedGC: Out of memoy!\n");
7600  exit(1);
7601  }
7602  biddyNodeTable.table[0] = (BiddyNode *) biddyTerminal;
7603 
7604  /* PROFILING */
7605  /*
7606  printf("(size=%u)(gcr=%.2f)(rr=%.2f)",biddyNodeTable.size,biddyNodeTable.gcratio,biddyNodeTable.resizeratio);
7607  */
7608  }
7609 
7610  /* PROFILING */
7611  /*
7612  else {
7613  printf("+");
7614  }
7615  */
7616 
7617  /* CHECK ALL LISTS AND IF RESIZE THEN PUT ALL KEPT NODES ALSO TO THE NEW NODE TABLE */
7618  /* BECAUSE OF REHASHING (NODES ARE STORED IN NODE TABLE IN 'ORDERED' LISTS) */
7619  /* IT IS REQUIRED TO VISIT NODES STARTING WITH THE LAST VARIABLE! */
7620  /* LAST VARIABLE IS NOT THE SAME AS THE SMALLEST/LARGEST IN THE VARIABLE ORDERING! */
7621  /* OBSOLETE NODES ARE REMOVED FROM LISTS */
7622  for (v=biddyVariableTable.num-1; v>0; v--) {
7623 
7624  /* DEBUGGING - !!! PRINTF THE NUMBER OF OBSOLETE NODES PER VARIABLE !!! */
7625  /*
7626  printf("GC VARIABLE %u (NODES: %u, OBSOLETE NODES: %u)\n",v,biddyVariableTable.table[v].num,biddyVariableTable.table[v].numobsolete);
7627  */
7628 
7629  /* if (v >= targetLT) or (v < targetGEQ) then no action is required because */
7630  /* there should be no obsolete nodes with (v >= targetLT) or (v < targetGEQ) */
7631  /* please note, that resize is not allowed if (targetLT != 0) */
7632  /* (targetLT != 0) is used in the next 'if' for evaluation speed, only */
7633  if ((targetLT != 0) && (!BiddyIsSmaller(biddyOrderingTable,v,targetLT) || BiddyIsSmaller(biddyOrderingTable,v,targetGEQ))) continue;
7634 
7635  /* IF RESIZE THEN ALL NODES EXCEPT THE FIRST ONE MUST BE VISITED */
7636  if (resizeRequired) {
7637  biddyVariableTable.table[v].numobsolete = biddyVariableTable.table[v].num - 1;
7638  }
7639 
7640  /* BE CAREFULLY WITH TYPE BiddyNode !!!! */
7641  /* FIELDS 'prev' AND 'next' HAVE TO BE THE FIRST AND THE SECOND! */
7642  /* THIS COMPUTATION USE SOME TRICKS! */
7643 
7644  if (biddyVariableTable.table[v].numobsolete) {
7645 
7646  /* UPDATING NODE TABLE */
7647  /* there is always at least one node in the list and the first node is never obsolete */
7648  tmpnode1 = biddyVariableTable.table[v].firstNode;
7649  assert( BiddyIsOK(tmpnode1) );
7650 
7651  biddyVariableTable.table[v].lastNode->list = NULL;
7652 
7653  /* the first node in the list is variable/element */
7654  /* and because it is not stored in Node table it does not need rehashing */
7655  tmpnode2 = (BiddyNode *) tmpnode1->list;
7656 
7657  while (biddyVariableTable.table[v].numobsolete) {
7658 
7659  /* DEBUGGING */
7660  /*
7661  printf(" GC WHILE OBSOLETE NODES = %u\n",biddyVariableTable.table[v].numobsolete);
7662  */
7663 
7664  assert( tmpnode2 != NULL) ;
7665  assert( tmpnode2->v == v ) ;
7666 
7667  if (!(tmpnode2->expiry) || (tmpnode2->expiry >= biddySystemAge)) {
7668  /* fortified, fresh or prolonged node */
7669  tmpnode1 = tmpnode2;
7670 
7671  /* if resize is required then this node must be rehashed and stored into new Node table */
7672  if (resizeRequired) {
7673  hash = nodeTableHash(v,tmpnode2->f,tmpnode2->t,biddyNodeTable.size);
7674  addNodeTable(MNG,hash,tmpnode2,NULL); /* add node to hash table */
7675  (biddyVariableTable.table[v].numobsolete)--; /* if resize is required then all nodes are counted with this counter */
7676  }
7677 
7678  } else {
7679 
7680  /* if targetLT is used then */
7681  /* there should not exist obsolete nodes with variable equal or higher than targetLT */
7682  /* and variable smaller than targetGEQ */
7683  /* in fact, nodes with obsolete 'expiry' may exist but only because */
7684  /* they have not been prolonged - they must not be removed! */
7685  assert( (targetLT == 0) || (BiddyIsSmaller(biddyOrderingTable,v,targetLT) && !BiddyIsSmaller(biddyOrderingTable,v,targetGEQ)) ) ;
7686 
7687  /* DEBUGGING */
7688  /*
7689  printf("REMOVE %p\n",(void *)tmpnode2);
7690  */
7691 
7692  /* obsolete node */
7693  cacheOK = FALSE;
7694  (biddyNodeTable.num)--;
7695  (biddyVariableTable.table[v].num)--;
7696  (biddyVariableTable.table[v].numobsolete)--;
7697  /* if resize is not required then remove from Node table */
7698  if (!resizeRequired) {
7699  tmpnode2->prev->next = tmpnode2->next;
7700  if (tmpnode2->next) {
7701  tmpnode2->next->prev = tmpnode2->prev;
7702  }
7703  }
7704  /* update list of live nodes */
7705  tmpnode1->list = (BiddyNode *) tmpnode2->list;
7706  /* insert obsolete node to the list of free nodes */
7707  tmpnode2->list = (void *) biddyFreeNodes;
7708  biddyFreeNodes = tmpnode2;
7709  }
7710 
7711  tmpnode2 = (BiddyNode *) tmpnode1->list;
7712  }
7713  if (!tmpnode1->list) {
7714  biddyVariableTable.table[v].lastNode = tmpnode1;
7715  }
7716  }
7717 
7718  }
7719  }
7720 
7721  /* DEBUGGING */
7722  /*
7723  else {
7724  printf("#");
7725  }
7726  */
7727 
7728  /* Updating cache tables - only if needed */
7729  if (!cacheOK) {
7730  c = biddyCacheList;
7731  while (c) {
7732  c->gc(MNG);
7733  c = c->next;
7734  }
7735  }
7736 
7737  /* DEBUGGING */
7738  /*
7739  printf("GC FINISHED: systemAge = %u, there are %u BDD nodes, NodeTableSize = %u\n",
7740  biddySystemAge,biddyNodeTable.num,biddyNodeTable.size);
7741  */
7742 
7743  /* DEBUGGING */
7744  /*
7745  if (purge) {
7746  for (v=1; v<biddyVariableTable.num; v++) {
7747  biddyVariableTable.table[v].lastNode->list = NULL;
7748  sup = biddyVariableTable.table[v].firstNode;
7749  while (sup) {
7750  if ((sup->expiry) && (sup->expiry < biddySystemAge)) {
7751  printf("BiddyManagedGC:: INVALID OBSOLETE NODE!\n");
7752  exit(1);
7753  }
7754  sup = (BiddyNode *) sup->list;
7755  }
7756  }
7757  }
7758  */
7759 
7760  /* GC calls used during sifting are not counted */
7761  if (targetLT == 0) {
7762  biddyNodeTable.gctime += clock() - starttime;
7763  }
7764 }
7765 
7766 /***************************************************************************/
7775 void
7776 BiddyManagedClean(Biddy_Manager MNG)
7777 {
7778  Biddy_Variable v;
7779 
7780  assert( MNG );
7781 
7782  /* DISCARD ALL NODES WHICH ARE NOT PRESERVED */
7783  /* implemented by simple increasing of biddySystemAge */
7784  BiddyIncSystemAge(MNG);
7785 
7786  /* to ensure that parameters in external functions are never obsolete, */
7787  /* constant functions must be explicitly refreshed, here */
7788  BiddyRefresh(biddyZero);
7789  BiddyRefresh(biddyOne);
7790 
7791  /* to ensure that parameters in external functions are never obsolete, */
7792  /* all variables and elements must be explicitly refreshed, here */
7793  for (v = 1; v < biddyVariableTable.num; v++) {
7794  if (biddyVariableTable.table[v].variable) BiddyRefresh(biddyVariableTable.table[v].variable);
7795  if (biddyVariableTable.table[v].element) BiddyRefresh(biddyVariableTable.table[v].element);
7796  }
7797 
7798  /* all obsolete formulae are labeled as deleted */
7799  for (v = 2; v < biddyFormulaTable.size; v++) {
7800  if (biddyFormulaTable.table[v].expiry && (biddyFormulaTable.table[v].expiry < biddySystemAge)) {
7801  biddyFormulaTable.table[v].deleted = TRUE;
7802  }
7803  }
7804 }
7805 
7806 /***************************************************************************/
7815 void
7816 BiddyManagedPurge(Biddy_Manager MNG)
7817 {
7818  assert( MNG );
7819 
7820  BiddyManagedGC(MNG,0,0,TRUE,TRUE); /* purge = TRUE, total = TRUE */
7821 }
7822 
7823 /***************************************************************************/
7832 void
7833 BiddyManagedPurgeAndReorder(Biddy_Manager MNG, Biddy_Edge f,
7834  Biddy_Boolean converge)
7835 {
7836  assert( MNG );
7837 
7838  BiddyManagedPurge(MNG);
7839  BiddyManagedSifting(MNG,f,converge);
7840 }
7841 
7842 /***************************************************************************/
7851 void
7852 BiddyManagedAddCache(Biddy_Manager MNG, Biddy_GCFunction gc)
7853 {
7854  BiddyCacheList *sup;
7855 
7856  assert( MNG );
7857 
7858  if (!biddyCacheList) {
7859 
7860  if (!(biddyCacheList = (BiddyCacheList *) malloc(sizeof(BiddyCacheList)))) {
7861  fprintf(stdout,"BiddyManagedAddCache: Out of memoy!\n");
7862  exit(1);
7863  }
7864 
7865  biddyCacheList->gc = gc;
7866  biddyCacheList->next = NULL;
7867  } else {
7868  sup = biddyCacheList;
7869  while (sup->next) sup = sup->next;
7870 
7871  if (!(sup->next = (BiddyCacheList *) malloc(sizeof(BiddyCacheList)))) {
7872  fprintf(stdout,"BiddyManagedAddCache: Out of memoy!\n");
7873  exit(1);
7874  }
7875 
7876  sup = sup->next;
7877  sup->gc = gc;
7878  sup->next = NULL;
7879  }
7880 }
7881 
7882 /***************************************************************************/
7891 unsigned int
7892 BiddyManagedAddFormula(Biddy_Manager MNG, Biddy_String x, Biddy_Edge f, int c)
7893 {
7894  unsigned int i;
7895  Biddy_Boolean OK;
7896  BiddyFormula *tmp;
7897  Biddy_Edge old;
7898 
7899  assert( MNG );
7900 
7901  /* DEBUGGING */
7902  /*
7903  if (x) {
7904  printf("BiddyManagedAddFormula: Formula %s\n",x);
7905  }
7906  */
7907 
7908  /* DEBUGGING */
7909  /*
7910  if (!x) {
7911  printf("BiddyManagedAddFormula: Anonymous formula with top variable %s\n",BiddyManagedGetTopVariableName(MNG,f));
7912  }
7913  */
7914 
7915  /*
7916  if (f && !BiddyIsOK(f)) {
7917  fprintf(stdout,"ERROR (BiddyManagedAddFormula): Bad f\n");
7918  free((void *)1);
7919  exit(1);
7920  }
7921  */
7922 
7923  if (c == -1) {
7924  c = biddySystemAge;
7925  }
7926  else if (c) {
7927  if ((c+biddySystemAge) < biddySystemAge) {
7928  BiddyCompactSystemAge(MNG);
7929  }
7930  c += biddySystemAge;
7931  }
7932 
7933  /* if formula does not have a name and is NULL or constant function, */
7934  /* then it will not be added, such BDD is already fortified, redundancy not needed */
7935  if (!x && (BiddyIsNull(f) || (f == biddyZero) || (f == biddyOne))) {
7936  return 0;
7937  }
7938 
7939  /* if formula does not have a name and it is the same as a basic variable/element, */
7940  /* then it will not be added, such BDD is already fortified, redundancy not needed */
7941  if (!x && !BiddyIsNull(f)) {
7942  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
7943  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
7944  {
7945  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
7946  return 0;
7947  }
7948  }
7949 #ifndef COMPACT
7950  else if ((biddyManagerType == BIDDYTYPEZBDD) || (biddyManagerType == BIDDYTYPEZFDD))
7951  {
7952  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
7953  return 0;
7954  }
7955  }
7956  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZFDDC))
7957  {
7958  if ((BiddyE(f) == biddyTerminal) && (BiddyT(f) == biddyTerminal)) {
7959  return 0;
7960  }
7961  }
7962  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
7963  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
7964  {
7965  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
7966  return 0;
7967  }
7968  }
7969 #endif
7970  }
7971 
7972  /* SEARCH IN THE FORMULA TABLE */
7973  if (!x) {
7974  OK = FALSE;
7975  i = biddyFormulaTable.size; /* tmp formulae (without name) are added on the end of the table */
7976  } else {
7977  OK = BiddyManagedFindFormula(MNG,x,&i,&old);
7978  }
7979 
7980  /* DEBUGGING */
7981  /*
7982  printf("BiddyManagedAddFormula: biddyFormulaTable.size = %u, findFormula returned %u, OK = %u\n",biddyFormulaTable.size,i,OK);
7983  */
7984 
7985  /* the first two formulae ("0" and "1") must not be changed */
7986  if (OK && (i<2))
7987  {
7988  printf("WARNING (BiddyManagedAddFormula): formula %s not added because it has the same name as the existing constant!\n",x);
7989  return i;
7990  }
7991 
7992  /* element found */
7993  if (OK) {
7994  /* printf("BiddyManagedAddFormula: element found %s!\n",x); */
7995 
7996  /* need to change persistent formula - new formula will be created */
7997  if (!biddyFormulaTable.table[i].expiry) {
7998  /* printf("BiddyManagedAddFormula: change permanently preserved formula %s!\n",x); */
7999  if (!biddyFormulaTable.table[i].deleted) {
8000  biddyFormulaTable.table[i].deleted = TRUE;
8001  i++;
8002  OK = FALSE;
8003  } else {
8004  printf("BiddyManagedAddFormula: Problem with deleted persistent function %s!\n",x);
8005  exit(1);
8006  }
8007  }
8008 
8009  /* need to change preserved formula - new formula will be created */
8010  else if (biddyFormulaTable.table[i].expiry > biddySystemAge) {
8011  /* printf("BiddyManagedAddFormula: change preserved formula %s!\n",x); */
8012  if (!biddyFormulaTable.table[i].deleted) {
8013  biddyFormulaTable.table[i].deleted = TRUE;
8014  i++;
8015  OK = FALSE;
8016  } else {
8017  printf("BiddyManagedAddFormula: Problem with deleted preserved function %s!\n",x);
8018  exit(1);
8019  }
8020  }
8021 
8022  }
8023 
8024  /* element can be reused */
8025  if (OK) {
8026  /* printf("BiddyManagedAddFormula: Formula %s OVERWRITTEN!\n",x); */
8027  biddyFormulaTable.table[i].f = f;
8028  biddyFormulaTable.table[i].expiry = (unsigned int) c;
8029  biddyFormulaTable.table[i].deleted = FALSE;
8030  if (!BiddyIsNull(f)) {
8031  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
8032  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
8033  {
8034  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
8035  /* this is variable, not changed */
8036  } else {
8037  BiddyProlongOne(f,(unsigned int) c);
8038  }
8039  }
8040 #ifndef COMPACT
8041  else if ((biddyManagerType == BIDDYTYPEZBDD) || (biddyManagerType == BIDDYTYPEZFDD))
8042  {
8043  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
8044  /* this is element, not changed */
8045  } else {
8046  BiddyProlongOne(f,(unsigned int) c);
8047  }
8048  }
8049  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZFDDC))
8050  {
8051  if ((BiddyE(f) == biddyTerminal) && (BiddyT(f) == biddyTerminal)) {
8052  /* this is element, not changed */
8053  }
8054  else {
8055  BiddyProlongOne(f, (unsigned int)c);
8056  }
8057  }
8058  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
8059  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
8060  {
8061  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
8062  /* this is variable/element, not changed */
8063  } else {
8064  BiddyProlongOne(f,(unsigned int) c);
8065  }
8066  }
8067 #endif
8068  }
8069  return i;
8070  }
8071 
8072  /* formula must be added, indices of the first two formulae must not be changed */
8073  if (i < 2) {
8074  printf("BiddyManagedAddFormula: Name of the formula must alphabetically be strictly greater than \"1\"!\n");
8075  exit(1);
8076  }
8077 
8078  biddyFormulaTable.size++;
8079  if (!(tmp = (BiddyFormula *)
8080  realloc(biddyFormulaTable.table,biddyFormulaTable.size*sizeof(BiddyFormula))))
8081  {
8082  printf("BiddyManagedAddFormula: Out of memoy!\n");
8083  exit(1);
8084  }
8085  biddyFormulaTable.table = tmp;
8086 
8087  /* DEBUGGING */
8088  /*
8089  printf("BiddyManagedAddFormula: biddyFormulaTable.size = %u, i = %u\n",biddyFormulaTable.size,i);
8090  */
8091 
8092  memmove(&biddyFormulaTable.table[i+1],&biddyFormulaTable.table[i],(biddyFormulaTable.size-i-1)*sizeof(BiddyFormula));
8093  /*
8094  for (j = biddyFormulaTable.size-1; j > i; j--) {
8095  biddyFormulaTable.table[j] = biddyFormulaTable.table[j-1];
8096  }
8097  */
8098 
8099  if (x) {
8100  biddyFormulaTable.table[i].name = strdup(x);
8101  biddyFormulaTable.numOrdered++;
8102  } else {
8103  biddyFormulaTable.table[i].name = NULL;
8104  }
8105  biddyFormulaTable.table[i].f = f;
8106  biddyFormulaTable.table[i].expiry = (unsigned int) c;
8107  biddyFormulaTable.table[i].deleted = FALSE;
8108  if (!BiddyIsNull(f)) {
8109  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
8110  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
8111  {
8112  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
8113  /* this is variable, not changed */
8114  } else {
8115  BiddyProlongOne(f,(unsigned int) c);
8116  }
8117  }
8118 #ifndef COMPACT
8119  else if ((biddyManagerType == BIDDYTYPEZBDD) || (biddyManagerType == BIDDYTYPEZFDD))
8120  {
8121  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
8122  /* this is element, not changed */
8123  } else {
8124  BiddyProlongOne(f,(unsigned int) c);
8125  }
8126  }
8127  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZFDDC))
8128  {
8129  if ((BiddyE(f) == biddyTerminal) && (BiddyT(f) == biddyTerminal)) {
8130  /* this is element, not changed */
8131  }
8132  else {
8133  BiddyProlongOne(f, (unsigned int)c);
8134  }
8135  }
8136  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
8137  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
8138  {
8139  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
8140  /* this is variable/element, not changed */
8141  } else {
8142  BiddyProlongOne(f,(unsigned int) c);
8143  }
8144  }
8145 #endif
8146  }
8147 
8148  /* DEBUGGING */
8149  /*
8150  printf("BiddyManagedAddFormula: biddySystemAge=%u, i=%d/%d, x=%s, c=%d, formula=%u, top=%u\n",biddySystemAge,i,biddyFormulaTable.size-1,x,c,biddyFormulaTable.table[i].expiry,BiddyN(f)->expiry);
8151  */
8152 
8153  /* DEBUGGING */
8154  /*
8155  printf("BiddyManagedAddFormula: biddySystemAge=%u, i=%d/%d, x=%s, f=%p\n",biddySystemAge,i,biddyFormulaTable.size-1,x,f);
8156  */
8157 
8158  if (!x) i = 0; /* if formula does not have a name return 0 */
8159 
8160  return i;
8161 }
8162 
8163 /***************************************************************************/
8173 BiddyManagedFindFormula(Biddy_Manager MNG, Biddy_String x,
8174  unsigned int *idx, Biddy_Edge *f)
8175 {
8176  unsigned int i,min,max;
8177  Biddy_Variable v;
8178  Biddy_Boolean OK;
8179  int cc;
8180 
8181  assert( MNG );
8182 
8183  *idx = 0;
8184  *f = biddyNull;
8185  if (!x) return FALSE;
8186 
8187  assert ( biddyFormulaTable.table );
8188 
8189  if (!strcmp(x,biddyFormulaTable.table[0].name)) { /* [0] = biddyZero */
8190  *idx = 0;
8191  *f = biddyZero;
8192  return TRUE;
8193  }
8194 
8195  if (!strcmp(x,biddyFormulaTable.table[1].name)) { /* [1] = biddyOne */
8196  *idx = 1;
8197  *f = biddyOne;
8198  return TRUE;
8199  }
8200 
8201  /* VARIABLES ARE CONSIDERED TO BE FORMULAE, [0] = constant variable 1 */
8202  v = 1;
8203  OK = FALSE;
8204  while (!OK && v<biddyVariableTable.num) {
8205  if (!strcmp(x,biddyVariableTable.table[v].name)) {
8206  OK = TRUE;
8207  } else {
8208  v++;
8209  }
8210  }
8211  if (OK) {
8212  *f = biddyVariableTable.table[v].variable;
8213  return TRUE;
8214  }
8215 
8216  /* NOT FOUND BECAUSE THERE ARE ONLY TWO FORMULAE, I.E. 0 AND 1 */
8217  if (biddyFormulaTable.numOrdered == 2) {
8218  *idx = 2;
8219  /* printf("BiddyManagedFindFormula: <%s> NOT FOUND!\n",x); */
8220  return FALSE;
8221  }
8222 
8223  /* VARIANT A: LINEAR SEARCH */
8224  /*
8225  OK = FALSE;
8226  for (i = 2; !OK && (i < biddyFormulaTable.numOrdered); i++) {
8227  if (biddyFormulaTable.table[i].name) {
8228  cc = strcmp(x,biddyFormulaTable.table[i].name);
8229  if ((cc == 0) && !biddyFormulaTable.table[i].deleted) {
8230  OK = TRUE;
8231  break;
8232  }
8233  if (cc < 0) break;
8234  } else {
8235  fprintf(stderr,"BiddyManagedFindFormula: Problem with the formula table!\n");
8236  exit(1);
8237  }
8238  }
8239  j = i;
8240  */
8241 
8242  /* VARIANT B: BINARY SEARCH */
8243  min = 2;
8244  max = biddyFormulaTable.numOrdered - 1;
8245 
8246  assert ( max <= biddyFormulaTable.size );
8247 
8248  /* DEBUGGING */
8249  /*
8250  fprintf(stderr,"biddyFormulaTable.size = %u, search for %s, min = %u (%s), max = %u (%s)\n",
8251  biddyFormulaTable.size,x,min,biddyFormulaTable.table[min].name,max,biddyFormulaTable.table[max].name);
8252  */
8253 
8254  cc = strcmp(x,biddyFormulaTable.table[min].name);
8255  if ((cc == 0) && !biddyFormulaTable.table[min].deleted) {
8256  i = min;
8257  OK = TRUE;
8258  } else if (cc < 0) {
8259  i = min;
8260  OK = FALSE;
8261  } else {
8262  cc = strcmp(x,biddyFormulaTable.table[max].name);
8263  if ((cc == 0) && !biddyFormulaTable.table[max].deleted) {
8264  i = max;
8265  OK = TRUE;
8266  } else if (cc > 0) {
8267  i = max+1;
8268  OK = FALSE;
8269  } else {
8270  i = (min + max) / 2;
8271  while (i != min) {
8272  cc = strcmp(x,biddyFormulaTable.table[i].name);
8273  if ((cc == 0) && !biddyFormulaTable.table[i].deleted) {
8274  min = max = i;
8275  OK = TRUE;
8276  } else if (cc < 0) {
8277  max = i;
8278  } else {
8279  min = i;
8280  }
8281  i = (min + max) / 2;
8282  }
8283  if (!OK) i++;
8284  }
8285  }
8286 
8287  /* DEBUGGING */
8288  /*
8289  if (i != j) {
8290  fprintf(stderr,"ERROR, i=%u, j=%u\n",i,j);
8291  for (i = 2; !OK && (i < biddyFormulaTable.numOrdered); i++) {
8292  fprintf(stderr,"%i. %s\n",i,biddyFormulaTable.table[i].name);
8293  }
8294  exit(1);
8295  }
8296  */
8297 
8298  if (OK) {
8299 
8300  /* element found */
8301  *idx = i;
8302  *f = biddyFormulaTable.table[i].f;
8303 
8304  /* DEBUGGING */
8305  /*
8306  printf("BiddyManagedFindFormula: FOUND i=%d, x=%s, f=%p\n",i,x,*f);
8307  */
8308 
8309  } else {
8310 
8311  /* element not found */
8312  *idx = i;
8313 
8314  /* DEBUGGING */
8315  /*
8316  printf("BiddyManagedFindFormula: <%s> NOT FOUND!\n",x);
8317  */
8318 
8319  }
8320 
8321  assert ( *idx <= biddyFormulaTable.size );
8322 
8323  return OK;
8324 }
8325 
8326 /***************************************************************************/
8336 BiddyManagedDeleteFormula(Biddy_Manager MNG, Biddy_String x)
8337 {
8338  unsigned int i;
8339  Biddy_Boolean OK;
8340  int cc;
8341 
8342  assert( MNG );
8343 
8344  if (!x) {
8345  printf("WARNING (BiddyManagedDeleteFormula): empty name!\n");
8346  return FALSE;
8347  }
8348 
8349  OK = FALSE;
8350 
8351  if (!biddyFormulaTable.table) {
8352  i = 0;
8353  } else {
8354  for (i = 0; !OK && (i < biddyFormulaTable.numOrdered); i++) {
8355  if (biddyFormulaTable.table[i].name) {
8356  cc = strcmp(x,biddyFormulaTable.table[i].name);
8357  if ((cc == 0) && !biddyFormulaTable.table[i].deleted) {
8358  OK = TRUE;
8359  break;
8360  }
8361  if (cc < 0) break;
8362  } else {
8363  fprintf(stderr,"BiddyManagedDeleteFormula: Problem with the formula table!\n");
8364  exit(1);
8365  }
8366  }
8367  }
8368 
8369  if (OK) {
8370  OK = BiddyManagedDeleteIthFormula(MNG,i);
8371  }
8372 
8373  return OK;
8374 }
8375 
8376 /***************************************************************************/
8386 BiddyManagedDeleteIthFormula(Biddy_Manager MNG, unsigned int i)
8387 {
8388  Biddy_Boolean OK;
8389 
8390  assert( MNG );
8391 
8392  /* the first two formulae ("0" and "1") must not be deleted */
8393  if (i<2) {
8394  OK = FALSE;
8395  } else {
8396  OK = TRUE;
8397  }
8398 
8399  if (OK) {
8400  /* formulae representing variables must not be deleted */
8401  if (BiddyIsNull(biddyFormulaTable.table[i].f) ||
8402  !biddyFormulaTable.table[i].name ||
8403  strcmp(biddyFormulaTable.table[i].name,
8404  BiddyManagedGetTopVariableName(MNG,biddyFormulaTable.table[i].f)))
8405  {
8406 
8407  /* DEBUGGING */
8408  /*
8409  if (biddyFormulaTable.table[i].name) {
8410  fprintf(stderr,"BiddyManagedDeleteIthFormula: Deleted %s\n",biddyFormulaTable.table[i].name);
8411  exit(1);
8412  }
8413  */
8414 
8415  /* this can be removed */
8416  biddyFormulaTable.table[i].deleted = TRUE;
8417  } else {
8418  OK = FALSE;
8419  }
8420  }
8421 
8422  return OK;
8423 }
8424 
8425 /***************************************************************************/
8434 Biddy_Edge
8435 BiddyManagedGetIthFormula(Biddy_Manager MNG, unsigned int i)
8436 {
8437  assert( MNG );
8438 
8439  if (!biddyFormulaTable.table) return biddyNull;
8440  if (i >= biddyFormulaTable.size) return biddyNull;
8441 
8442  return biddyFormulaTable.table[i].f;
8443 }
8444 
8445 /***************************************************************************/
8455 BiddyManagedGetIthFormulaName(Biddy_Manager MNG, unsigned int i)
8456 {
8457  Biddy_String name;
8458 
8459  assert( MNG );
8460 
8461  if (!biddyFormulaTable.table) return NULL;
8462  if (i >= biddyFormulaTable.size) return NULL;
8463 
8464  if (biddyFormulaTable.table[i].deleted) {
8465  name = biddyFormulaTable.deletedName;
8466  } else {
8467  name = biddyFormulaTable.table[i].name;
8468  }
8469 
8470  return name;
8471 }
8472 
8473 /***************************************************************************/
8483 BiddyManagedGetOrdering(Biddy_Manager MNG)
8484 {
8485  Biddy_Variable v,k;
8486  Biddy_String varname,result;
8487 
8488  assert( MNG );
8489 
8490  varname = (Biddy_String) malloc(255);
8491  result = strdup("");
8492 
8493  v = BiddyManagedGetLowestVariable(MNG);
8494  for (k = 0; k < biddyVariableTable.num; k++) {
8495  sprintf(varname,"\"%s\"",biddyVariableTable.table[v].name);
8496  concat(&result,varname);
8497  if (k != biddyVariableTable.num-1) concat(&result,",");
8498  v = biddyVariableTable.table[v].next;
8499  }
8500 
8501  free(varname);
8502 
8503  return result;
8504 }
8505 
8506 /***************************************************************************/
8515 void
8516 BiddyManagedSetOrdering(Biddy_Manager MNG, Biddy_String ordering)
8517 {
8518  Biddy_String varname;
8519  Biddy_Variable v;
8520  unsigned int n;
8521 
8522  assert( MNG );
8523 
8524  if (ordering[0] != '\"') {
8525  printf("WARNING: BiddyManagedSetOrdering got wrong ordering string!\n");
8526  }
8527 
8528  n = 1;
8529  varname = strtok(ordering,"\"");
8530  while (varname) {
8531  if (varname) {
8532  /* printf("SET ORDERING: %s\n",varname); */
8533  v = BiddyManagedGetVariable(MNG,varname);
8534  if (v) {
8535  free(biddyVariableTable.table[v].data);
8536  biddyVariableTable.table[v].data = (void *) malloc(sizeof(Biddy_Variable));
8537  *((Biddy_Variable *)biddyVariableTable.table[v].data) = n++;
8538  }
8539  }
8540  varname = strtok(NULL,"\"");varname = strtok(NULL,"\"");
8541  }
8542 
8543  BiddySetOrderingByData(MNG);
8544  BiddyManagedClearVariablesData(MNG);
8545 }
8546 
8547 /***************************************************************************/
8556 void
8557 BiddyManagedSetAlphabeticOrdering(Biddy_Manager MNG)
8558 {
8559  BiddyOrderingTable *table;
8560 
8561  assert( MNG );
8562 
8563 /* TO DO: MORE EFFICIENT WOULD BE TO USE BiddySetOrderingByData */
8564  table = (BiddyOrderingTable *) malloc(sizeof(BiddyOrderingTable));
8565  alphabeticOrdering(MNG,*table);
8566  BiddySetOrdering(MNG,*table);
8567  free(table);
8568 }
8569 
8570 /***************************************************************************/
8580 BiddyManagedSwapWithHigher(Biddy_Manager MNG, Biddy_Variable v)
8581 {
8582  Biddy_Boolean active;
8583 
8584  assert( MNG );
8585 
8586  /* OBSOLETE NODES ARE REMOVED BEFORE SWAPPING */
8587  BiddyManagedAutoGC(MNG);
8588 
8589  return swapWithHigher(MNG,v,&active);
8590 }
8591 
8592 /***************************************************************************/
8602 BiddyManagedSwapWithLower(Biddy_Manager MNG, Biddy_Variable v)
8603 {
8604  Biddy_Boolean active;
8605 
8606  assert( MNG );
8607 
8608  /* OBSOLETE NODES ARE REMOVED BEFORE SWAPPING */
8609  BiddyManagedAutoGC(MNG);
8610 
8611  return swapWithLower(MNG,v,&active);
8612 }
8613 
8614 /***************************************************************************/
8624 BiddyManagedSifting(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean converge)
8625 {
8626  Biddy_Boolean DEBUGGING = FALSE;
8627  Biddy_Boolean status;
8628  clock_t starttime;
8629 
8630  assert( MNG );
8631 
8632  /*
8633  if (!checkFunctionOrdering(MNG,f)) {
8634  printf("ERROR!!!\n");
8635  }
8636  */
8637 
8638  assert( (f == NULL) || (BiddyIsOK(f) == TRUE) );
8639 
8640  /* DEBUGGING */
8641  /*
8642  printf("SIFTING START: num sifting: %u\n",BiddyManagedNodeTableSiftingNumber(MNG));
8643  */
8644 
8645  /* DEBUGGING */
8646 
8647  if (DEBUGGING)
8648  {
8649  Biddy_Variable n;
8650  printf("========================================\n");
8651  printf("SIFTING START: num sifting: %u\n",BiddyManagedNodeTableSiftingNumber(MNG));
8652  printf("SIFTING START: num swapping: %u\n",BiddyManagedNodeTableSwapNumber(MNG));
8653  printf("SIFTING START: num garbage collection: %u\n",BiddyManagedNodeTableGCNumber(MNG));
8654  if (f) {
8655  BiddyFormula formula;
8656  printf("MINIMIZING NODE NUMBER FOR THE GIVEN FUNCTION\n");
8657  for (n=0;n<biddyFormulaTable.size;n++) {
8658  formula = biddyFormulaTable.table[n];
8659  if (formula.f == f) {
8660  if (formula.name) {
8661  printf("Formula name: %s\n",formula.name);
8662  } else {
8663  printf("Formula name: NULL\n");
8664  }
8665  }
8666  }
8667  printf("Initial number of dependent variables: %u\n",BiddyManagedDependentVariableNumber(MNG,f,FALSE));
8668  printf("Initial number of minterms: %.0f\n",BiddyManagedCountMinterms(MNG,f,0));
8669  printf("Initial number of nodes: %u\n",BiddyManagedCountNodes(MNG,f));
8670  printf("Top edge: %p\n",(void *) f);
8671  printf("Top variable: %s\n",BiddyManagedGetTopVariableName(MNG,f));
8672  printf("Expiry value of top node: %d\n",((BiddyNode *) BiddyP(f))->expiry);
8673  }
8674  printf("SIFTING: initial order\n");
8675  writeORDER(MNG);
8676  for (n = 1; n < biddyFormulaTable.size; n++) {
8677  if (!biddyFormulaTable.table[n].deleted &&
8678  !BiddyIsNull(biddyFormulaTable.table[n].f) &&
8679  !BiddyIsTerminal(biddyFormulaTable.table[n].f))
8680  {
8681  assert( BiddyIsOK(biddyFormulaTable.table[n].f) );
8682  }
8683  }
8684  printf("========================================\n");
8685  }
8686 
8687 
8688  /* DEBUGGING */
8689  /*
8690  if (DEBUGGING) {
8691  BiddySystemReport(MNG);
8692  }
8693  */
8694 
8695  biddyNodeTable.sifting++;
8696  starttime = clock();
8697 
8698  /* DELETE ALL CACHE TABLES AND DISABLE THEM */
8699  /* TO DO: user cache tables are not considered, yet */
8700  BiddyOPGarbageDeleteAll(MNG);
8701  BiddyEAGarbageDeleteAll(MNG);
8702  BiddyRCGarbageDeleteAll(MNG);
8703  BiddyReplaceGarbageDeleteAll(MNG);
8704  biddyOPCache.disabled = TRUE;
8705  biddyEACache.disabled = TRUE;
8706  biddyRCCache.disabled = TRUE;
8707  biddyReplaceCache.disabled = TRUE;
8708 
8709  /* OBSOLETE NODES WOULD MAKE THE APPLICATION OF SIFTING LESS EFFICIENT */
8710  /* WE DO NOT WANT TO USE PURGE HERE BECAUSE IT LIMITS THE USABILITY OF SIFTING */
8711  BiddyManagedForceGC(MNG); /* imediatelly remove obsolete nodes */
8712 
8713  if (!f) {
8714  /* MINIMIZING NODE NUMBER FOR THE WHOLE SYSTEM */
8715  status = BiddyGlobalSifting(MNG,converge);
8716  } else {
8717  /* MINIMIZING NODE NUMBER FOR THE GIVEN FUNCTION */
8718  status = BiddySiftingOnFunction(MNG,f,converge);
8719  }
8720 
8721  /* ENABLE ALL CACHE TABLES */
8722  /* TO DO: user caches are not considered, yet */
8723  biddyOPCache.disabled = FALSE;
8724  biddyEACache.disabled = FALSE;
8725  biddyRCCache.disabled = FALSE;
8726  biddyReplaceCache.disabled = FALSE;
8727 
8728  biddyNodeTable.drtime += clock() - starttime;
8729 
8730  /* DEBUGGING */
8731 
8732  if (DEBUGGING)
8733  {
8734  Biddy_Variable n;
8735  printf("========================================\n");
8736  printf("SIFTING FINISH: num sifting: %u\n",BiddyManagedNodeTableSiftingNumber(MNG));
8737  printf("SIFTING FINISH: num swapping: %u\n",BiddyManagedNodeTableSwapNumber(MNG));
8738  printf("SIFTING FINISH: num garbage collection: %u\n",BiddyManagedNodeTableGCNumber(MNG));
8739  if (f) {
8740  printf("Final number of dependent variables: %u\n",BiddyManagedDependentVariableNumber(MNG,f,FALSE));
8741  printf("Final number of minterms: %.0f\n",BiddyManagedCountMinterms(MNG,f,0));
8742  printf("Final number of nodes: %u\n",BiddyManagedCountNodes(MNG,f));
8743  printf("Top edge: %p\n",(void *) f);
8744  printf("Top variable: %s\n",BiddyManagedGetTopVariableName(MNG,f));
8745  printf("Expiry value of top node: %d\n",((BiddyNode *) BiddyP(f))->expiry);
8746  }
8747  printf("SIFTING: final order\n");
8748  writeORDER(MNG);
8749  for (n = 1; n < biddyFormulaTable.size; n++) {
8750  if (!biddyFormulaTable.table[n].deleted &&
8751  !BiddyIsNull(biddyFormulaTable.table[n].f) &&
8752  !BiddyIsTerminal(biddyFormulaTable.table[n].f))
8753  {
8754  assert( BiddyIsOK(biddyFormulaTable.table[n].f) );
8755  }
8756  }
8757  printf("========================================\n");
8758  }
8759 
8760 
8761  /* DEBUGGING */
8762  /*
8763  if (DEBUGGING) {
8764  BiddySystemReport(MNG);
8765  }
8766  */
8767 
8768  /* biddySiftingActive = FALSE; */
8769 
8770  return status; /* sifting has been performed */
8771 }
8772 
8773 /***************************************************************************/
8782 void
8783 BiddyManagedMinimizeBDD(Biddy_Manager MNG, Biddy_String name)
8784 {
8785  Biddy_Edge f;
8786  unsigned int idx;
8787  unsigned int n,MIN;
8788  BiddyOrderingTable *finalOrdering;
8789  Biddy_Boolean first;
8790 
8791  assert( MNG );
8792 
8793  /* DEBUGGING */
8794  /*
8795  if (BiddyManagedFindFormula(MNG,name,&idx,&f)) {
8796  printf("MINIMIZE FOR %s STARTED\n",name);
8797  n = BiddyManagedCountNodes(MNG,f);
8798  printf("START: n=%u\n",n);
8799  } else {
8800  printf("MINIMIZE: FORMULA %s NOT FOUND\n",name);
8801  }
8802  */
8803 
8804  /* TO DO: create a copy in new manager and minimize it there! */
8805 
8806  finalOrdering = (BiddyOrderingTable *) malloc(sizeof(BiddyOrderingTable));
8807 
8808  BiddySjtInit(MNG);
8809 
8810  MIN = 0;
8811  first = TRUE;
8812  do {
8813  BiddyManagedFindFormula(MNG,name,&idx,&f);
8814 
8815  /* use this to minimize the number of internal nodes */
8816  /*
8817  n = 0;
8818  BiddyManagedSelectNode(MNG,biddyTerminal);
8819  BiddyNodeNumber(MNG,f,&n);
8820  BiddyManagedDeselectAll(MNG);
8821  */
8822 
8823  /* use this to minimize the number of all nodes */
8824 
8825  n = BiddyManagedCountNodes(MNG,f);
8826 
8827 
8828  /* DEBUGGING */
8829  /*
8830  printf("MINIMIZATION STEP: n=%u\n",n);
8831  */
8832 
8833  if (first || (n < MIN)) {
8834  MIN = n;
8835  memcpy(*finalOrdering,biddyOrderingTable,sizeof(BiddyOrderingTable));
8836  }
8837 
8838  first = FALSE;
8839 
8840  } while(BiddySjtStep(MNG));
8841 
8842  BiddySjtExit(MNG);
8843 
8844  BiddySetOrdering(MNG,*finalOrdering);
8845 
8846  free(finalOrdering);
8847 
8848  /* DEBUGGING */
8849  /*
8850  BiddyManagedFindFormula(MNG,name,&idx,&f);
8851  n = BiddyManagedCountNodes(MNG,f);
8852  printf("FINAL: n=%u\n",n);
8853  */
8854 }
8855 
8856 /***************************************************************************/
8865 void
8866 BiddyManagedMaximizeBDD(Biddy_Manager MNG, Biddy_String name)
8867 {
8868  Biddy_Edge f;
8869  unsigned int idx;
8870  unsigned int n,MAX;
8871  BiddyOrderingTable *finalOrdering;
8872 
8873  assert( MNG );
8874 
8875  /* DEBUGGING */
8876  /*
8877  if (BiddyManagedFindFormula(MNG,name,&idx,&f)) {
8878  printf("MAXIMIZE FOR %s STARTED\n",name);
8879  n = BiddyManagedCountNodes(MNG,f);
8880  printf("START: n=%u\n",n);
8881  } else {
8882  printf("MAXIMIZE: FORMULA %s NOT FOUND\n",name);
8883  }
8884  */
8885 
8886  /* TO DO: create a copy in new manager and minimize it there! */
8887 
8888  finalOrdering = (BiddyOrderingTable *) malloc(sizeof(BiddyOrderingTable));
8889 
8890  BiddySjtInit(MNG);
8891  MAX = 0;
8892  do {
8893  BiddyManagedFindFormula(MNG,name,&idx,&f);
8894 
8895  /* use this to maximize the number of internal nodes */
8896  /*
8897  n = 0;
8898  BiddyManagedSelectNode(MNG,biddyTerminal);
8899  BiddyNodeNumber(MNG,f,&n);
8900  BiddyManagedDeselectAll(MNG);
8901  */
8902 
8903  /* use this to maximize the number of all nodes */
8904 
8905  n = BiddyManagedCountNodes(MNG,f);
8906 
8907 
8908  /* DEBUGGING */
8909  /*
8910  printf("MAXIMIZATION STEP: n=%u\n",n);
8911  */
8912 
8913  if (!MAX || (n > MAX)) {
8914  MAX = n;
8915  memcpy(*finalOrdering,biddyOrderingTable,sizeof(BiddyOrderingTable));
8916  }
8917  } while(BiddySjtStep(MNG));
8918 
8919  BiddySjtExit(MNG);
8920 
8921  BiddySetOrdering(MNG,*finalOrdering);
8922 
8923  free(finalOrdering);
8924 
8925  /* DEBUGGING */
8926  /*
8927  BiddyManagedFindFormula(MNG,name,&idx,&f);
8928  n = BiddyManagedCountNodes(MNG,f);
8929  printf("FINAL: n=%u\n",n);
8930  */
8931 }
8932 
8933 /***************************************************************************/
8946 Biddy_Edge
8947 BiddyManagedCopy(Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_Edge f,
8948  Biddy_Boolean complete)
8949 {
8950  Biddy_Edge r;
8951  Biddy_Variable v1,v2,k;
8952  Biddy_String vname;
8953  Biddy_Boolean simplecopy;
8954 #ifndef COMPACT
8955  Biddy_Variable j,top,prevvar;
8956  Biddy_String topname;
8957 #endif
8958 
8959  assert( MNG1 );
8960  assert( MNG2 );
8961 
8962  if (MNG1 == MNG2) {
8963  return f;
8964  }
8965 
8966  /* CHECK IF THE TARGET MNG IS EMPTY */
8967  simplecopy = FALSE;
8968  if (biddyVariableTable2.num == 1) {
8969  simplecopy = TRUE;
8970  }
8971 
8972  /* DEBUGGING */
8973  /*
8974  printf("BiddyManagedCopy before domain\n");
8975  BiddySystemReport(MNG2);
8976  */
8977 
8978  /* COPY THE DOMAIN */
8979  /* the ordering of the new variable is determined in BiddyInitMNG */
8980  /* FOR OBDDs AND OFDDs: new variable is added below (bottommore) all others */
8981  /* FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: new variable is added above (topmore) all others */
8982  /* USING BiddyManagedGetVariableName, FINAL ORDER FOR OBDDs AND OFDDs WILL BE: [1] < [2] < ... < [size-1] < [0] */
8983  /* USING BiddyManagedGetVariableName, FINAL ORDER FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs WILL BE: [size-1] < [size-2] < ... < [1] < [0] */
8984  /* BY USING VARIOUS COPYING METHODS WE ACHIEVE THE SAME FINAL ORDERING FOR DIFFERENT TARGET MANAGERS */
8985  /* IF simplecopy THEN WE ARE ALSO ABLE TO ACHIEVE THE CONSINSTENCY OF VARIABLE POSITIONS */
8986  /* IF simplecopy AND !complete THEN element edges for OBDDs and TZBDDs and variable edges for ZBDDs are not created */
8987  if ((biddyManagerType2 == BIDDYTYPEOBDDC) || (biddyManagerType2 == BIDDYTYPEOBDD) ||
8988  (biddyManagerType2 == BIDDYTYPEOFDDC) || (biddyManagerType2 == BIDDYTYPEOFDD))
8989  {
8990 #ifndef COMPACT
8991  if (simplecopy && (
8992  (biddyManagerType1 == BIDDYTYPEZBDDC) || (biddyManagerType1 == BIDDYTYPEZBDD) ||
8993  (biddyManagerType1 == BIDDYTYPEZFDDC) || (biddyManagerType1 == BIDDYTYPEZFDD) ||
8994  (biddyManagerType1 == BIDDYTYPETZBDDC) || (biddyManagerType1 == BIDDYTYPETZBDD) ||
8995  (biddyManagerType1 == BIDDYTYPETZFDDC) || (biddyManagerType1 == BIDDYTYPETZFDD))
8996  )
8997  {
8998  /* keep the consinstency of variable positions for ZBDD -> ROBDD and TZBDD -> ROBDD */
8999  v1 = 0;
9000  for (k = 1; k < biddyVariableTable1.num; k++) {
9001  v1 = biddyVariableTable1.table[v1].prev;
9002  vname = BiddyManagedGetVariableName(MNG1,v1);
9003  v2 = BiddyManagedFoaVariable(MNG2,vname,TRUE,complete); /* create variable and optionaly element */
9004  /* v2 = BiddyManagedAddVariableByName(MNG2,vname); */ /* target is OBDD, thus create variable, only */
9005  BiddyManagedSetVariableData(MNG2,v2,BiddyManagedGetVariableData(MNG1,v1));
9006  for (j = 1; j < k; j++) {
9007  BiddyManagedSwapWithLower(MNG2,v2); /* move up */
9008  }
9009  }
9010  } else
9011 #endif
9012  {
9013  v1 = BiddyManagedGetLowestVariable(MNG1); /* lowest = topmost */
9014  for (k = 1; k < biddyVariableTable1.num; k++) {
9015  vname = BiddyManagedGetVariableName(MNG1,v1);
9016  v2 = BiddyManagedFoaVariable(MNG2,vname,TRUE,complete); /* create variable and optionaly element */
9017  /* v2 = BiddyManagedAddVariableByName(MNG2,vname); */ /* target is OBDD, thus create variable, only */
9018  v2 = BiddyManagedAddVariableByName(MNG2,vname); /* TO DO: IS VARIABLE ORDERING OK? */
9019  BiddyManagedSetVariableData(MNG2,v2,BiddyManagedGetVariableData(MNG1,v1));
9020  v1 = biddyVariableTable1.table[v1].next;
9021  }
9022  }
9023  }
9024 
9025 #ifndef COMPACT
9026  else if ((biddyManagerType2 == BIDDYTYPEZBDDC) || (biddyManagerType2 == BIDDYTYPEZBDD) ||
9027  (biddyManagerType2 == BIDDYTYPEZFDDC) || (biddyManagerType2 == BIDDYTYPEZFDD) ||
9028  (biddyManagerType2 == BIDDYTYPETZBDDC) || (biddyManagerType2 == BIDDYTYPETZBDD) ||
9029  (biddyManagerType2 == BIDDYTYPETZFDDC) || (biddyManagerType2 == BIDDYTYPETZFDD))
9030  {
9031  if (simplecopy && (
9032  (biddyManagerType1 == BIDDYTYPEOBDDC) || (biddyManagerType1 == BIDDYTYPEOBDD) ||
9033  (biddyManagerType1 == BIDDYTYPEOFDDC) || (biddyManagerType1 == BIDDYTYPEOFDD))
9034  )
9035  {
9036  /* keep the consinstency of variable positions for ROBDD -> ZBDD and ROBDD -> TZBDD */
9037  v1 = BiddyManagedGetLowestVariable(MNG1); /* lowest = topmost */
9038  for (k = 1; k < biddyVariableTable1.num; k++) {
9039  vname = BiddyManagedGetVariableName(MNG1,v1);
9040  v2 = BiddyManagedFoaVariable(MNG2,vname,FALSE,complete); /* create element and optionaly variable */
9041  /* v2 = BiddyManagedAddElementByName(MNG2,vname); */ /* target is OBDD, thus create element, only */
9042  BiddyManagedSetVariableData(MNG2,v2,BiddyManagedGetVariableData(MNG1,v1));
9043  v1 = biddyVariableTable1.table[v1].next;
9044  for (j = 1; j < k; j++) {
9045  BiddyManagedSwapWithHigher(MNG2,v2); /* move down */
9046  }
9047  /* DEBUGGING */
9048  /*
9049  {
9050  Biddy_Variable w;
9051  printf("GLOBAL ORDERING AFTER COPY: ");
9052  for (w=0; w<biddyVariableTable2.num; w++) {
9053  printf("<%s(%u)-%u>",biddyVariableTable2.table[w].name,w,getGlobalOrdering(MNG2,w));
9054  }
9055  printf("\n");
9056  }
9057  */
9058  }
9059  } else {
9060  v1 = 0;
9061  for (k = 1; k < biddyVariableTable1.num; k++) {
9062  v1 = biddyVariableTable1.table[v1].prev;
<