Biddy  1.8.1
An academic Binary Decision Diagrams package
biddyStat.c
Go to the documentation of this file.
1 /***************************************************************************/
43 #include "biddyInt.h"
44 
45 #ifdef BIDDYEXTENDEDSTATS_YES
46 #include "math.h"
47 #endif
48 
49 /*----------------------------------------------------------------------------*/
50 /* Static function prototypes */
51 /*----------------------------------------------------------------------------*/
52 
53 static void MaxLevel(Biddy_Edge f, unsigned int *max, unsigned int i);
54 
55 static void AvgLevel(Biddy_Edge f, float *sum, unsigned int *n, unsigned int i);
56 
57 static void pathCount(Biddy_Manager MNG, Biddy_Edge f, unsigned long long int *c1, unsigned long long int *c0, Biddy_Boolean *cf);
58 
59 static void mintermCount(Biddy_Manager MNG, Biddy_Edge f, mpz_t max, mpz_t result, Biddy_Boolean *leftmost);
60 
61 static unsigned int nodePlainNumber(Biddy_Manager MNG, Biddy_Edge f);
62 
63 static float calculateSD(unsigned long long int *data, unsigned int n);
64 
65 /*----------------------------------------------------------------------------*/
66 /* Definition of exported functions */
67 /*----------------------------------------------------------------------------*/
68 
69 /***************************************************************************/
80 #ifdef __cplusplus
81 extern "C" {
82 #endif
83 
84 unsigned int
86 {
87  unsigned int n;
88 
89  if (!MNG) MNG = biddyAnonymousManager;
90 
91  if (Biddy_IsNull(f)) return 0;
92  if (Biddy_IsTerminal(f)) return 1;
93 
94  if (biddyManagerType == BIDDYTYPEOBDD) {
95  /* IMPLEMENTED */
96  /* terminal 0 is represented by complemented edge to terminal 1 */
97  n = 2; /* BOTH TERMINAL NODES ARE COUNTED HERE */
98  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
99  /* IMPLEMENTED */
100  n = 1; /* TERMINAL NODE IS COUNTED HERE */
101  } else if (biddyManagerType == BIDDYTYPEZBDD) {
102  /* IMPLEMENTED */
103  /* terminal 0 is represented by complemented edge to terminal 1 */
104  /* TO DO: we do not need exact number of complemented edges here */
105  n = 0;
106  Biddy_Managed_SelectNode(MNG,biddyTerminal); /* needed for BiddyComplementedEdgeNumber */
107  BiddyComplementedEdgeNumber(MNG,f,&n);
109  if (n == 0) {
110  n = 1; /* TERMINAL NODE IS COUNTED HERE */
111  }
112  else {
113  n = 2; /* BOTH TERMINAL NODES ARE COUNTED HERE */
114  }
115  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
116  /* IMPLEMENTED */
117  n = 1; /* TERMINAL NODE IS COUNTED HERE */
118  } else if (biddyManagerType == BIDDYTYPETZBDD) {
119  /* IMPLEMENTED */
120  /* terminal 0 is represented by complemented edge to terminal 1 */
121  /* TO DO: we do not need exact number of complemented edges here */
122  n = 0;
123  Biddy_Managed_SelectNode(MNG,biddyTerminal); /* needed for BiddyComplementedEdgeNumber */
124  BiddyComplementedEdgeNumber(MNG,f,&n);
126  if (n == 0) {
127  n = 1; /* TERMINAL NODE IS COUNTED HERE */
128  } else {
129  n = 2; /* BOTH TERMINAL NODES ARE COUNTED HERE */
130  }
131  } else if (biddyManagerType == BIDDYTYPETZBDDC) {
132  /* IMPLEMENTED */
133  n = 1; /* TERMINAL NODE IS COUNTED HERE */
134  } else {
135  fprintf(stderr,"Biddy_CountNodes: Unsupported BDD type!\n");
136  return 0;
137  }
138 
139  Biddy_Managed_SelectNode(MNG,biddyTerminal); /* needed for BiddyNodeNumber */
140  BiddyNodeNumber(MNG,f,&n);
142 
143  return n;
144 }
145 
146 #ifdef __cplusplus
147 }
148 #endif
149 
150 /***************************************************************************/
159 #ifdef __cplusplus
160 extern "C" {
161 #endif
162 
163 unsigned int
165 {
166  unsigned int max;
167 
168  if (Biddy_IsNull(f)) return 0;
169 
170  max = 0;
171  MaxLevel(f,&max,0);
172  return max;
173 }
174 
175 #ifdef __cplusplus
176 }
177 #endif
178 
179 /***************************************************************************/
191 #ifdef __cplusplus
192 extern "C" {
193 #endif
194 
195 float
197 {
198  float sum;
199  unsigned int n;
200 
201  if (Biddy_IsNull(f)) return 0;
202 
203  sum = 0;
204  n = 0;
205  AvgLevel(f,&sum,&n,0);
206  return (sum/n);
207 }
208 
209 #ifdef __cplusplus
210 }
211 #endif
212 
213 /***************************************************************************/
223 #ifdef __cplusplus
224 extern "C" {
225 #endif
226 
229 {
230  if (!MNG) MNG = biddyAnonymousManager;
231 
232  return biddyVariableTable.num;
233 }
234 
235 #ifdef __cplusplus
236 }
237 #endif
238 
239 /***************************************************************************/
248 #ifdef __cplusplus
249 extern "C" {
250 #endif
251 
252 unsigned int
254 {
255  if (!MNG) MNG = biddyAnonymousManager;
256 
257  /* THE REAL SIZE OF NODE TABLE IS biddyNodeTable.size+2. */
258  /* THE FIRST INDEX IS NOT USED, */
259  /* THUS WE HAVE biddyNodeTable.size+1 USEFUL ELEMENTS. */
260 
261  return biddyNodeTable.size+1;
262 }
263 
264 #ifdef __cplusplus
265 }
266 #endif
267 
268 /***************************************************************************/
278 #ifdef __cplusplus
279 extern "C" {
280 #endif
281 
282 unsigned int
284 {
285  if (!MNG) MNG = biddyAnonymousManager;
286 
287  return biddyNodeTable.blocknumber;
288 }
289 
290 #ifdef __cplusplus
291 }
292 #endif
293 
294 /***************************************************************************/
303 #ifdef __cplusplus
304 extern "C" {
305 #endif
306 
307 unsigned int
309 {
310  if (!MNG) MNG = biddyAnonymousManager;
311 
312  return biddyNodeTable.generated;
313 }
314 
315 #ifdef __cplusplus
316 }
317 #endif
318 
319 /***************************************************************************/
329 #ifdef __cplusplus
330 extern "C" {
331 #endif
332 
333 unsigned int
335 {
336  if (!MNG) MNG = biddyAnonymousManager;
337 
338  return biddyNodeTable.max;
339 }
340 
341 #ifdef __cplusplus
342 }
343 #endif
344 
345 /***************************************************************************/
355 #ifdef __cplusplus
356 extern "C" {
357 #endif
358 
359 unsigned int
361 {
362  if (!MNG) MNG = biddyAnonymousManager;
363 
364  return biddyNodeTable.num;
365 }
366 
367 #ifdef __cplusplus
368 }
369 #endif
370 
371 /***************************************************************************/
381 #ifdef __cplusplus
382 extern "C" {
383 #endif
384 
385 unsigned int
387 {
388  if (!MNG) MNG = biddyAnonymousManager;
389 
390  return biddyVariableTable.table[v].num;
391 }
392 
393 #ifdef __cplusplus
394 }
395 #endif
396 
397 /***************************************************************************/
407 #ifdef __cplusplus
408 extern "C" {
409 #endif
410 
411 unsigned int
413 {
414  if (!MNG) MNG = biddyAnonymousManager;
415 
416  return biddyNodeTable.nodetableresize;
417 }
418 
419 #ifdef __cplusplus
420 }
421 #endif
422 
423 /***************************************************************************/
433 #ifdef __cplusplus
434 extern "C" {
435 #endif
436 
437 unsigned long long int
439 {
440  unsigned long long int foa = 0;
441 
442  if (!MNG) MNG = biddyAnonymousManager;
443 
444 #ifdef BIDDYEXTENDEDSTATS_YES
445  foa = biddyNodeTable.foa;
446 #endif
447 
448  return foa;
449 }
450 
451 #ifdef __cplusplus
452 }
453 #endif
454 
455 /***************************************************************************/
465 #ifdef __cplusplus
466 extern "C" {
467 #endif
468 
469 unsigned long long int
471 {
472  unsigned long long int find = 0;
473 
474  if (!MNG) MNG = biddyAnonymousManager;
475 
476 #ifdef BIDDYEXTENDEDSTATS_YES
477  find = biddyNodeTable.find;
478 #endif
479 
480  return find;
481 }
482 
483 #ifdef __cplusplus
484 }
485 #endif
486 
487 /***************************************************************************/
497 #ifdef __cplusplus
498 extern "C" {
499 #endif
500 
501 unsigned long long int
503 {
504  unsigned long long int compare = 0;
505 
506  if (!MNG) MNG = biddyAnonymousManager;
507 
508 #ifdef BIDDYEXTENDEDSTATS_YES
509  compare = biddyNodeTable.compare;
510 #endif
511 
512  return compare;
513 }
514 
515 #ifdef __cplusplus
516 }
517 #endif
518 
519 /***************************************************************************/
529 #ifdef __cplusplus
530 extern "C" {
531 #endif
532 
533 unsigned long long int
535 {
536  unsigned long long int add = 0;
537 
538  if (!MNG) MNG = biddyAnonymousManager;
539 
540 #ifdef BIDDYEXTENDEDSTATS_YES
541  add = biddyNodeTable.add;
542 #endif
543 
544  return add;
545 }
546 
547 #ifdef __cplusplus
548 }
549 #endif
550 
551 /***************************************************************************/
560 #ifdef __cplusplus
561 extern "C" {
562 #endif
563 
564 unsigned int
566 {
567  if (!MNG) MNG = biddyAnonymousManager;
568 
569  return biddyNodeTable.garbage;
570 }
571 
572 #ifdef __cplusplus
573 }
574 #endif
575 
576 /***************************************************************************/
585 #ifdef __cplusplus
586 extern "C" {
587 #endif
588 
589 unsigned int
591 {
592  if (!MNG) MNG = biddyAnonymousManager;
593 
594  return (1000*biddyNodeTable.gctime)/(1*CLOCKS_PER_SEC);
595 }
596 
597 #ifdef __cplusplus
598 }
599 #endif
600 
601 /***************************************************************************/
614 #ifdef __cplusplus
615 extern "C" {
616 #endif
617 
618 unsigned long long int
620 {
621  unsigned long long int gcobsolete = 0;
622 
623 #ifdef BIDDYEXTENDEDSTATS_YES
624  unsigned int i;
625  unsigned long long int sum;
626 
627  if (!MNG) MNG = biddyAnonymousManager;
628 
629  sum = 0;
630  for (i = 0; i < biddyNodeTable.garbage; i++) {
631  sum += biddyNodeTable.gcobsolete[i];
632  }
633  gcobsolete = sum;
634  calculateSD(biddyNodeTable.gcobsolete,biddyNodeTable.garbage);
635 #endif
636 
637  return gcobsolete;
638 }
639 
640 #ifdef __cplusplus
641 }
642 #endif
643 
644 /***************************************************************************/
653 #ifdef __cplusplus
654 extern "C" {
655 #endif
656 
657 unsigned int
659 {
660  if (!MNG) MNG = biddyAnonymousManager;
661 
662  return biddyNodeTable.swap;
663 }
664 
665 #ifdef __cplusplus
666 }
667 #endif
668 
669 /***************************************************************************/
679 #ifdef __cplusplus
680 extern "C" {
681 #endif
682 
683 unsigned int
685 {
686  if (!MNG) MNG = biddyAnonymousManager;
687 
688  return biddyNodeTable.sifting;
689 }
690 
691 #ifdef __cplusplus
692 }
693 #endif
694 
695 /***************************************************************************/
704 #ifdef __cplusplus
705 extern "C" {
706 #endif
707 
708 unsigned int
710 {
711  if (!MNG) MNG = biddyAnonymousManager;
712 
713  return (1000*biddyNodeTable.drtime)/(1*CLOCKS_PER_SEC);
714 }
715 
716 #ifdef __cplusplus
717 }
718 #endif
719 
720 /***************************************************************************/
729 #ifdef __cplusplus
730 extern "C" {
731 #endif
732 
733 unsigned int
735 {
736  if (!MNG) MNG = biddyAnonymousManager;
737 
738  return biddyNodeTable.funite;
739 }
740 
741 #ifdef __cplusplus
742 }
743 #endif
744 
745 /***************************************************************************/
757 #ifdef __cplusplus
758 extern "C" {
759 #endif
760 
761 unsigned long long int
763 {
764  unsigned long long int iterecursive = 0;
765 
766  if (!MNG) MNG = biddyAnonymousManager;
767 
768 #ifdef BIDDYEXTENDEDSTATS_YES
769  iterecursive = biddyNodeTable.iterecursive;
770 #endif
771 
772  return iterecursive;
773 }
774 
775 #ifdef __cplusplus
776 }
777 #endif
778 
779 /***************************************************************************/
789 #ifdef __cplusplus
790 extern "C" {
791 #endif
792 
793 unsigned int
795 {
796  if (!MNG) MNG = biddyAnonymousManager;
797 
798  return biddyNodeTable.funandor;
799 }
800 
801 #ifdef __cplusplus
802 }
803 #endif
804 
805 /***************************************************************************/
817 #ifdef __cplusplus
818 extern "C" {
819 #endif
820 
821 unsigned long long int
823 {
824  unsigned long long int andorrecursive = 0;
825 
826  if (!MNG) MNG = biddyAnonymousManager;
827 
828 #ifdef BIDDYEXTENDEDSTATS_YES
829  andorrecursive = biddyNodeTable.andorrecursive;
830 #endif
831 
832  return andorrecursive;
833 }
834 
835 #ifdef __cplusplus
836 }
837 #endif
838 
839 /***************************************************************************/
848 #ifdef __cplusplus
849 extern "C" {
850 #endif
851 
852 unsigned int
854 {
855  if (!MNG) MNG = biddyAnonymousManager;
856 
857  return biddyNodeTable.funxor;
858 }
859 
860 #ifdef __cplusplus
861 }
862 #endif
863 
864 /***************************************************************************/
876 #ifdef __cplusplus
877 extern "C" {
878 #endif
879 
880 unsigned long long int
882 {
883  unsigned long long int xorrecursive = 0;
884 
885  if (!MNG) MNG = biddyAnonymousManager;
886 
887 #ifdef BIDDYEXTENDEDSTATS_YES
888  xorrecursive = biddyNodeTable.xorrecursive;
889 #endif
890 
891  return xorrecursive;
892 }
893 
894 #ifdef __cplusplus
895 }
896 #endif
897 
898 /***************************************************************************/
908 #ifdef __cplusplus
909 extern "C" {
910 #endif
911 
912 unsigned int
914 {
915  if (!MNG) MNG = biddyAnonymousManager;
916 
917  return biddyFormulaTable.size;
918 }
919 
920 #ifdef __cplusplus
921 }
922 #endif
923 
924 /***************************************************************************/
933 #ifdef __cplusplus
934 extern "C" {
935 #endif
936 
937 unsigned int
939 {
940  unsigned int i,n;
941 
942  if (!MNG) MNG = biddyAnonymousManager;
943 
944  n = 0;
945  for (i=1; i<=biddyNodeTable.size+1; i++) {
946  if (biddyNodeTable.table[i] != NULL) {
947  n++;
948  }
949  }
950  return n;
951 }
952 
953 #ifdef __cplusplus
954 }
955 #endif
956 
957 /***************************************************************************/
966 #ifdef __cplusplus
967 extern "C" {
968 #endif
969 
970 unsigned int
972 {
973  unsigned int i,n,max;
974  BiddyNode *sup;
975 
976  /* DEBUG */
977  /*
978  unsigned maxi;
979  */
980 
981  if (!MNG) MNG = biddyAnonymousManager;
982 
983  max = 0;
984  for (i=1; i<=biddyNodeTable.size+1; i++) {
985  if (biddyNodeTable.table[i] != NULL) {
986  n = 0;
987  sup = biddyNodeTable.table[i];
988  while (sup != NULL) {
989  n++;
990  assert( sup != sup->next );
991  sup = sup->next;
992  }
993  if (n > max) {
994  max = n;
995 
996  /* DEBUG */
997  /*
998  maxi = i;
999  */
1000  }
1001  }
1002  }
1003 
1004  /* DEBUG */
1005  /*
1006  sup = biddyNodeTable.table[maxi];
1007  printf("MAX LIST (%u):\n",maxi);
1008  while (sup != NULL) {
1009  printf("v=%u, else=%p, then=%p\n",sup->v,(void*)sup->f,(void*)sup->t);
1010  sup = sup->next;
1011  }
1012  */
1013 
1014  return max;
1015 }
1016 
1017 #ifdef __cplusplus
1018 }
1019 #endif
1020 
1021 /***************************************************************************/
1030 #ifdef __cplusplus
1031 extern "C" {
1032 #endif
1033 
1034 float
1036 {
1037  float sum;
1038  unsigned int i,n;
1039  BiddyNode *sup;
1040 
1041  if (!MNG) MNG = biddyAnonymousManager;
1042 
1043  sum = 0;
1044  n = 0;
1045  for (i=1; i<=biddyNodeTable.size+1; i++) {
1046  if (biddyNodeTable.table[i] != NULL) {
1047  n++;
1048  sup = biddyNodeTable.table[i];
1049  while (sup != NULL) {
1050  sum = sum + 1;
1051  assert( sup != sup->next );
1052  sup = sup->next;
1053  }
1054  }
1055  }
1056  return (sum/n);
1057 }
1058 
1059 #ifdef __cplusplus
1060 }
1061 #endif
1062 
1063 /***************************************************************************/
1072 #ifdef __cplusplus
1073 extern "C" {
1074 #endif
1075 
1076 unsigned long long int
1078 {
1079  if (!MNG) MNG = biddyAnonymousManager;
1080 
1081  return *(biddyOPCache.search);
1082 }
1083 
1084 #ifdef __cplusplus
1085 }
1086 #endif
1087 
1088 /***************************************************************************/
1097 #ifdef __cplusplus
1098 extern "C" {
1099 #endif
1100 
1101 unsigned long long int
1103 {
1104  if (!MNG) MNG = biddyAnonymousManager;
1105 
1106  return *(biddyOPCache.find);
1107 }
1108 
1109 #ifdef __cplusplus
1110 }
1111 #endif
1112 
1113 /***************************************************************************/
1122 #ifdef __cplusplus
1123 extern "C" {
1124 #endif
1125 
1126 unsigned long long int
1128 {
1129  unsigned long long int insert = 0;
1130 
1131  if (!MNG) MNG = biddyAnonymousManager;
1132 
1133 #ifdef BIDDYEXTENDEDSTATS_YES
1134  insert = *(biddyOPCache.insert);
1135 #endif
1136 
1137  return insert;
1138 }
1139 
1140 #ifdef __cplusplus
1141 }
1142 #endif
1143 
1144 /***************************************************************************/
1153 #ifdef __cplusplus
1154 extern "C" {
1155 #endif
1156 
1157 unsigned long long int
1159 {
1160  unsigned long long int overwrite = 0;
1161 
1162  if (!MNG) MNG = biddyAnonymousManager;
1163 
1164 #ifdef BIDDYEXTENDEDSTATS_YES
1165  overwrite = *(biddyOPCache.overwrite);
1166 #endif
1167 
1168  return overwrite;
1169 }
1170 
1171 #ifdef __cplusplus
1172 }
1173 #endif
1174 
1175 /***************************************************************************/
1186 #ifdef __cplusplus
1187 extern "C" {
1188 #endif
1189 
1190 unsigned int
1192 {
1193  unsigned int n;
1194 
1195  if (!MNG) MNG = biddyAnonymousManager;
1196 
1197  if (Biddy_IsNull(f)) return 0;
1198 
1199  if (biddyManagerType == BIDDYTYPEOBDD) {
1200  /* IMPLEMENTED */
1201  /* terminal 0 is represented by complemented edge to terminal 1 */
1202  return Biddy_Managed_CountNodes(MNG,f);
1203  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1204  /* IMPLEMENTED */
1205  n = 2; /* BOTH TERMINAL NODES ARE COUNTED HERE */
1206  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1207  /* IMPLEMENTED */
1208  /* terminal 0 is represented by complemented edge to terminal 1 */
1209  return Biddy_Managed_CountNodes(MNG,f);
1210  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1211  /* IMPLEMENTED */
1212  /* terminal 0 is represented by complemented edge to terminal 1 */
1213  /* TO DO: we do not need exact number of complemented edges here */
1214  if (Biddy_IsTerminal(f)) {
1215  n = 0;
1216  } else {
1217  if (Biddy_GetMark(f)) {
1218  n = 1;
1219  } else {
1220  n = 0;
1221  Biddy_Managed_SelectNode(MNG,biddyTerminal); /* needed for BiddyComplementedEdgeNumber */
1222  BiddyComplementedEdgeNumber(MNG,f,&n);
1224  }
1225  }
1226  if (n == 0) {
1227  n = 1; /* TERMINAL NODE IS COUNTED HERE */
1228  }
1229  else {
1230  n = 2; /* BOTH TERMINAL NODES ARE COUNTED HERE */
1231  }
1232  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1233  /* IMPLEMENTED */
1234  /* terminal 0 is represented by complemented edge to terminal 1 */
1235  return Biddy_Managed_CountNodes(MNG,f);
1236  } else if (biddyManagerType == BIDDYTYPETZBDDC) {
1237  /* NOT IMPLEMENTED, YET */
1238  return 0;
1239  } else {
1240  fprintf(stderr,"Biddy_CountNodesPlain: Unsupported BDD type!\n");
1241  return 0;
1242  }
1243 
1244  if (Biddy_IsTerminal(f)) return 1;
1245 
1246  BiddyCreateLocalInfo(MNG,f);
1247  n += nodePlainNumber(MNG,f); /* select all nodes except terminal node */
1248  BiddyDeleteLocalInfo(MNG,f);
1249 
1250  return n;
1251 }
1252 
1253 #ifdef __cplusplus
1254 }
1255 #endif
1256 
1257 /***************************************************************************/
1274 #ifdef __cplusplus
1275 extern "C" {
1276 #endif
1277 
1278 unsigned int
1280  Biddy_Boolean select)
1281 {
1282  Biddy_Variable i;
1283  unsigned int n;
1284  unsigned int v;
1285 
1286  if (!MNG) MNG = biddyAnonymousManager;
1287 
1288  if (Biddy_IsNull(f)) return 0;
1289  if ((biddyManagerType != BIDDYTYPETZBDDC) && (biddyManagerType != BIDDYTYPETZBDD) &&
1290  (Biddy_IsTerminal(f))) return 0;
1291 
1292  /* variables should not be selected */
1293  /*
1294  for (i=1;i<biddyVariableTable.num;i++) {
1295  biddyVariableTable.table[i].selected = FALSE;
1296  }
1297  */
1298 
1299  v = 0;
1300  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1301  /* IMPLEMENTED */
1302  n = 1; /* NOT NEEDED, BUT NODES ARE ALSO COUNTED BY BiddyNodeVarNumber */
1303  Biddy_Managed_SelectNode(MNG,biddyTerminal); /* for OBDDs, this is needed for BiddyNodeVarNumber */
1304  BiddyNodeVarNumber(MNG,f,&n); /* DEPENDENT VARIABLES ARE MARKED, all nodes are selected */
1305  Biddy_Managed_DeselectAll(MNG); /* deselect all nodes */
1306  for (i=1;i<biddyVariableTable.num;i++) {
1307  if (biddyVariableTable.table[i].selected == TRUE) {
1308  v++;
1309  if (!select) biddyVariableTable.table[i].selected = FALSE; /* deselect variable */
1310  }
1311  }
1312  }
1313  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
1314  /* PROTOTYPED USING Restrict */
1315  /*
1316  for (i=1;i<biddyVariableTable.num;i++) {
1317  if (BiddyManagedRestrict(MNG,f,i,FALSE) != BiddyManagedRestrict(MNG,f,i,TRUE)) {
1318  v++;
1319  }
1320  }
1321  */
1322  /* IMPLEMENTED */
1323  BiddyCreateLocalInfo(MNG,f); /* FOR ZBDDs, localinfo IS USED BY BiddyNodeVarNumber */
1324  n = 1; /* NOT NEEDED, BUT NODES ARE ALSO COUNTED BY BiddyNodeVarNumber */
1325  BiddyNodeVarNumber(MNG,f,&n); /* DEPENDENT VARIABLES ARE MARKED, ALL NODES ARE SELECTED */
1326  BiddyDeleteLocalInfo(MNG,f); /* FOR ZBDDs, localinfo IS USED BY BiddyNodeVarNumber */
1327  v = 0;
1328  for (i=1;i<biddyVariableTable.num;i++) {
1329  if (BiddyIsSmaller(i,BiddyV(f)) || (biddyVariableTable.table[i].selected == TRUE))
1330  {
1331  v++;
1332  if (!select) biddyVariableTable.table[i].selected = FALSE; /* deselect variable */
1333  }
1334  }
1335  }
1336  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
1337  /* PROTOTYPED USING Restrict */
1338  /*
1339  for (i=1;i<biddyVariableTable.num;i++) {
1340  if (BiddyManagedRestrict(MNG,f,i,FALSE) != BiddyManagedRestrict(MNG,f,i,TRUE)) {
1341  v++;
1342  }
1343  }
1344  */
1345  /* IMPLEMENTED */
1346  n = 1; /* NOT NEEDED, BUT NODES ARE ALSO COUNTED BY BiddyNodeVarNumber */
1347  Biddy_Managed_SelectNode(MNG,biddyTerminal); /* for TZBDDs, this is needed for BiddyNodeVarNumber */
1348  BiddyNodeVarNumber(MNG,f,&n); /* DEPENDENT VARIABLES ARE MARKED, all nodes are selected */
1349  Biddy_Managed_DeselectAll(MNG); /* deselect all nodes */
1350  for (i=1;i<biddyVariableTable.num;i++) {
1351  if (biddyVariableTable.table[i].selected == TRUE) {
1352  v++;
1353  if (!select) biddyVariableTable.table[i].selected = FALSE; /* deselect variable */
1354  }
1355  }
1356  /* variables above the top variable which are equal or greater than the top tag are also dependent */
1357  i = Biddy_GetTag(f);
1358  while (BiddyIsSmaller(i,BiddyV(f))) {
1359  v++;
1360  if (select) biddyVariableTable.table[i].selected = TRUE; /* select variable */
1361  i = biddyVariableTable.table[i].next;
1362  }
1363  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
1364  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
1365  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
1366  {
1367  fprintf(stderr,"Biddy_DependentVariableNumber: this BDD type is not supported, yet!\n");
1368  return 0;
1369  } else {
1370  fprintf(stderr,"Biddy_DependentVariableNumber: Unsupported BDD type!\n");
1371  return 0;
1372  }
1373 
1374  return v;
1375 }
1376 
1377 #ifdef __cplusplus
1378 }
1379 #endif
1380 
1381 /***************************************************************************/
1396 #ifdef __cplusplus
1397 extern "C" {
1398 #endif
1399 
1400 unsigned int
1402 {
1403  unsigned int n;
1404 
1405  if (!MNG) MNG = biddyAnonymousManager;
1406 
1407  if (Biddy_IsNull(f)) return 0;
1408 
1409  if (biddyManagerType == BIDDYTYPEOBDD) {
1410  /* IMPLEMENTED */
1411  return 0;
1412  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1413  /* IMPLEMENTED */
1414  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1415  /* IMPLEMENTED */
1416  return 0;
1417  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1418  /* IMPLEMENTED */
1419  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1420  /* IMPLEMENTED */
1421  return 0;
1422  } else if (biddyManagerType == BIDDYTYPETZBDDC) {
1423  /* IMPLEMENTED */
1424  } else {
1425  fprintf(stderr,"Biddy_CountComplemented: Unsupported BDD type!\n");
1426  return 0;
1427  }
1428 
1429  n = 0;
1430  Biddy_Managed_SelectNode(MNG,biddyTerminal); /* needed for BiddyComplementedEdgeNumber */
1431  BiddyComplementedEdgeNumber(MNG,f,&n);
1433 
1434  return n;
1435 }
1436 
1437 #ifdef __cplusplus
1438 }
1439 #endif
1440 
1441 /***************************************************************************/
1452 #ifdef __cplusplus
1453 extern "C" {
1454 #endif
1455 
1456 unsigned long long int
1458 {
1459  unsigned long long int r1,r0;
1460  Biddy_Boolean rf;
1461 
1462  if (!MNG) MNG = biddyAnonymousManager;
1463 
1464  if (biddyManagerType == BIDDYTYPEOBDD) {
1465  /* IMPLEMENTED */
1466  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1467  /* IMPLEMENTED */
1468  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1469  /* IMPLEMENTED */
1470  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1471  /* IMPLEMENTED */
1472  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1473  /* IMPLEMENTED */
1474  } else if (biddyManagerType == BIDDYTYPETZBDDC)
1475  {
1476  fprintf(stderr,"Biddy_CountPaths: this BDD type is not supported, yet!\n");
1477  return 0;
1478  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
1479  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
1480  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
1481  {
1482  fprintf(stderr,"Biddy_CountPaths: this BDD type is not supported, yet!\n");
1483  return 0;
1484  } else {
1485  fprintf(stderr,"Biddy_CountPaths: Unsupported BDD type!\n");
1486  return 0;
1487  }
1488 
1489  if (Biddy_IsNull(f)) return 0;
1490  if (f == biddyZero) return 0;
1491  if (Biddy_IsTerminal(f)) return 1;
1492 
1493  BiddyCreateLocalInfo(MNG,f);
1494  pathCount(MNG,f,&r1,&r0,&rf); /* all nodes except terminal node are selected */
1495  BiddyDeleteLocalInfo(MNG,f);
1496 
1497  return r1;
1498 }
1499 
1500 #ifdef __cplusplus
1501 }
1502 #endif
1503 
1504 /***************************************************************************/
1521 #ifdef __cplusplus
1522 extern "C" {
1523 #endif
1524 
1525 double
1527 {
1528  unsigned int var,depvar;
1529  mpz_t max;
1530  mpz_t result;
1531  double resultd;
1532  Biddy_Boolean leftmost;
1533 
1534  if (!MNG) MNG = biddyAnonymousManager;
1535 
1536  if (biddyManagerType == BIDDYTYPEOBDD) {
1537  /* IMPLEMENTED */
1538  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1539  /* IMPLEMENTED */
1540  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1541  /* IMPLEMENTED */
1542  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1543  /* IMPLEMENTED */
1544  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1545  /* IMPLEMENTED */
1546  } else if (biddyManagerType == BIDDYTYPETZBDDC)
1547  {
1548  fprintf(stderr,"Biddy_CountMinterms: this BDD type is not supported, yet!\n");
1549  return 0.0;
1550  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
1551  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
1552  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
1553  {
1554  fprintf(stderr,"Biddy_CountMinterms: this BDD type is not supported, yet!\n");
1555  return 0.0;
1556  } else {
1557  fprintf(stderr,"Biddy_CountMinterms: Unsupported BDD type!\n");
1558  return 0.0;
1559  }
1560 
1561  if (Biddy_IsNull(f)) return 0;
1562  if (f == biddyZero) return 0;
1563 
1564  var = 0;
1565  depvar = 0;
1566  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1567  var = BiddyCreateLocalInfo(MNG,f); /* returns the number of noticeable variables */
1568  depvar = var; /* number of dependent variables is the same as the number of noticeable variables */
1569  }
1570  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
1571  depvar = Biddy_Managed_DependentVariableNumber(MNG,f,FALSE); /* for ZBDDs, this should be called before CreateLocalInfo! */
1572  var = BiddyCreateLocalInfo(MNG,f); /* returns the number of noticeable variables */
1573  }
1574  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
1575  depvar = Biddy_Managed_DependentVariableNumber(MNG,f,FALSE); /* for TZBDDs, this should be called before CreateLocalInfo! */
1576  var = BiddyCreateLocalInfo(MNG,f); /* returns the number of noticeable variables */
1577  }
1578 
1579  /* nvars is the requested number of variables */
1580  if (nvars == 0) nvars = depvar;
1581  if (nvars < depvar) {
1582  nvars = depvar;
1583  fprintf(stderr,"WARNING (Biddy_CountMinterms): nvars < depvar\n");
1584  }
1585 
1586  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1587  mpz_init(max);
1588  mpz_ui_pow_ui(max,2,var); /* initialized using the number of noticeable variables */
1589  leftmost = FALSE; /* it is not used */
1590  }
1591  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
1592  mpz_init(max); /* it is not used */
1593  leftmost = FALSE;
1594  }
1595  else if ((biddyManagerType == BIDDYTYPETZBDDC) ||(biddyManagerType == BIDDYTYPETZBDD)) {
1596  mpz_init(max);
1597  mpz_ui_pow_ui(max,2,var); /* initialized using the number of noticeable variables */
1598  leftmost = FALSE; /* it is not used */
1599  }
1600 
1601  mpz_init(result);
1602  mintermCount(MNG,f,max,result,&leftmost); /* select all nodes except terminal node */
1603 
1604  /* the obtained result considers the number of noticeable variables (var) */
1605  /* the result should be adapted to consider the requested number of variables (nvar) */
1606  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1607  /* the requested number of variables cannot be smaller than the number of noticeable variables */
1608  if (nvars > var) {
1609  while (nvars > var) {
1610  mpz_mul_ui(result,result,2);
1611  nvars--;
1612  }
1613  }
1614  }
1615  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
1616  /* the requested number of variables cannot be greater than the number of noticeable variables */
1617  if (nvars < var) {
1618  while (nvars < var) {
1619  mpz_divexact_ui(result,result,2);
1620  nvars++;
1621  }
1622  }
1623  }
1624  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
1625  if (nvars > var) {
1626  while (nvars > var) {
1627  mpz_mul_ui(result,result,2);
1628  nvars--;
1629  }
1630  }
1631  else if (nvars < var) {
1632  while (nvars < var) {
1633  mpz_divexact_ui(result,result,2);
1634  nvars++;
1635  }
1636  }
1637  }
1638 
1639  resultd = mpz_get_d(result);
1640  mpz_clear(max);
1641  mpz_clear(result);
1642 
1643  /* all nodes except terminal node are selected */
1644  BiddyDeleteLocalInfo(MNG,f);
1645 
1646  return resultd;
1647 }
1648 
1649 #ifdef __cplusplus
1650 }
1651 #endif
1652 
1653 /***************************************************************************/
1665 #ifdef __cplusplus
1666 extern "C" {
1667 #endif
1668 
1669 double
1671  unsigned int nvars)
1672 {
1673  double n;
1674  double m;
1675 
1676  if (!MNG) MNG = biddyAnonymousManager;
1677 
1678  if (Biddy_IsNull(f)) return 0.0;
1679  if (f == biddyZero) return 0.0;
1680 
1681  if (biddyManagerType == BIDDYTYPEOBDD) {
1682  /* IMPLEMENTED */
1683  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1684  /* IMPLEMENTED */
1685  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1686  /* IMPLEMENTED */
1687  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1688  /* IMPLEMENTED */
1689  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1690  /* IMPLEMENTED */
1691  } else if (biddyManagerType == BIDDYTYPETZBDDC)
1692  {
1693  fprintf(stderr,"Biddy_DensityOfFunction: this BDD type is not supported, yet!\n");
1694  return 0.0;
1695  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
1696  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
1697  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
1698  {
1699  fprintf(stderr,"Biddy_DensityOfFunction: this BDD type is not supported, yet!\n");
1700  return 0.0;
1701  } else {
1702  fprintf(stderr,"Biddy_DensityOfFunction: Unsupported BDD type!\n");
1703  return 0.0;
1704  }
1705 
1706  if (nvars == 0) {
1707  nvars = Biddy_Managed_DependentVariableNumber(MNG,f,FALSE);
1708  }
1709  m = Biddy_Managed_CountMinterms(MNG,f,nvars);
1710 
1711  n = 1.0;
1712  while (nvars) {
1713 
1714  assert( n < 2 * n );
1715 
1716  n = 2 * n;
1717  nvars--;
1718  }
1719 
1720  return m/n;
1721 }
1722 
1723 #ifdef __cplusplus
1724 }
1725 #endif
1726 
1727 /***************************************************************************/
1738 #ifdef __cplusplus
1739 extern "C" {
1740 #endif
1741 
1742 double
1744 {
1745  unsigned int n;
1746  double m;
1747 
1748  if (!MNG) MNG = biddyAnonymousManager;
1749 
1750  if (Biddy_IsNull(f)) return 0.0;
1751  if (f == biddyZero) return 0.0;
1752 
1753  if (biddyManagerType == BIDDYTYPEOBDD) {
1754  /* IMPLEMENTED */
1755  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1756  /* IMPLEMENTED */
1757  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1758  /* IMPLEMENTED */
1759  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1760  /* IMPLEMENTED */
1761  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1762  /* IMPLEMENTED */
1763  } else if (biddyManagerType == BIDDYTYPETZBDDC)
1764  {
1765  fprintf(stderr,"Biddy_DensityOfBDD: this BDD type is not supported, yet!\n");
1766  return 0.0;
1767  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
1768  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
1769  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
1770  {
1771  fprintf(stderr,"Biddy_DensityOfBDD: this BDD type is not supported, yet!\n");
1772  return 0.0;
1773  } else {
1774  fprintf(stderr,"Biddy_DensityOfBDD: Unsupported BDD type!\n");
1775  return 0.0;
1776  }
1777 
1778  if (nvars == 0) {
1779  Biddy_Variable i;
1780 
1781  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1782  n = 1;
1783  Biddy_Managed_SelectNode(MNG,biddyTerminal); /* for OBDDs, this is needed for BiddyNodeVarNumber */
1784  BiddyNodeVarNumber(MNG,f,&n); /* DEPENDENT VARIABLES ARE MARKED, all nodes are selected */
1785  Biddy_Managed_DeselectAll(MNG); /* for OBDDs, this is needed after BiddyNodeVarNumber */
1786  }
1787  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
1788  BiddyCreateLocalInfo(MNG,f); /* FOR ZBDDs, localinfo IS USED BY BiddyNodeVarNumber */
1789  n = 1;
1790  BiddyNodeVarNumber(MNG,f,&n); /* DEPENDENT VARIABLES ARE MARKED, selects all except terminal node */
1791  BiddyDeleteLocalInfo(MNG,f); /* this will deselect all nodes */
1792  }
1793  else if (biddyManagerType == BIDDYTYPETZBDD) {
1794  n = 1;
1795  Biddy_Managed_SelectNode(MNG,biddyTerminal); /* for TZBDDs, this is needed for BiddyNodeVarNumber */
1796  BiddyNodeVarNumber(MNG,f,&n); /* DEPENDENT VARIABLES ARE MARKED, all nodes are selected */
1797  Biddy_Managed_DeselectAll(MNG); /* for TZBDDs, this is needed after BiddyNodeVarNumber */
1798  }
1799 
1800  for (i=1;i<biddyVariableTable.num;i++) {
1801  if (biddyVariableTable.table[i].selected == TRUE) {
1802  nvars++;
1803  biddyVariableTable.table[i].selected = FALSE; /* deselect variable */
1804  }
1805  }
1806 
1807  } else {
1808 
1809  n = Biddy_Managed_CountNodes(MNG,f);
1810 
1811  }
1812 
1813  m = Biddy_Managed_CountMinterms(MNG,f,nvars);
1814  return m/n;
1815 }
1816 
1817 #ifdef __cplusplus
1818 }
1819 #endif
1820 
1821 /***************************************************************************/
1834 #ifdef __cplusplus
1835 extern "C" {
1836 #endif
1837 
1838 unsigned int
1840  Biddy_Manager MNG2;
1841  Biddy_Variable k,v;
1842  Biddy_String vname;
1843  unsigned int fidx;
1844  unsigned int n,num;
1845  Biddy_Boolean first;
1846 
1847  if (!MNG) MNG = biddyAnonymousManager;
1848 
1849  if (Biddy_IsNull(f)) return 0;
1850  if (f == biddyZero) return 1;
1851 
1852  num = Biddy_Managed_DependentVariableNumber(MNG,f,TRUE);
1853  if (num > 9) {
1854  printf("Biddy_Managed_MinNodes: Function has to many variables (%u)!\n",num);
1855  for (k = 0; k < biddyVariableTable.num; k++) {
1856  biddyVariableTable.table[k].selected = FALSE; /* deselect variable */
1857  }
1858  return 0;
1859  }
1860 
1861  num = 0;
1863 
1864  /* COPY THE DOMAIN - DEPENDENT VARIABLES ONLY */
1865  /* the ordering of the new variable is determined in Biddy_InitMNG */
1866  /* FOR OBDDs AND OFDDs: new variable is added below (bottommore) all others */
1867  /* FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: new variable is added above (topmore) all others */
1868  /* FINAL ORDER FOR OBDDs AND OFDDs: [1] < [2] < ... < [size-1] < [0] */
1869  /* FINAL ORDER FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: [size-1] < [size-2] < ... < [1] < [0] */
1870  if ((biddyManagerType2 == BIDDYTYPEOBDDC) || (biddyManagerType2 == BIDDYTYPEOBDD) ||
1871  (biddyManagerType2 == BIDDYTYPEOFDDC) || (biddyManagerType2 == BIDDYTYPEOFDD))
1872  {
1873  v = Biddy_Managed_GetLowestVariable(MNG); /* lowest = topmost */
1874  for (k = 1; k < biddyVariableTable.num; k++) {
1875  if (biddyVariableTable.table[v].selected == TRUE) {
1876  vname = Biddy_Managed_GetVariableName(MNG,v);
1877  Biddy_Managed_AddVariableByName(MNG2,vname);
1878  biddyVariableTable.table[v].selected = FALSE; /* deselect variable */
1879  }
1880  v = biddyVariableTable.table[v].next;
1881  }
1882  }
1883 
1884  else if ((biddyManagerType2 == BIDDYTYPEZBDDC) || (biddyManagerType2 == BIDDYTYPEZBDD) ||
1885  (biddyManagerType2 == BIDDYTYPEZFDDC) || (biddyManagerType2 == BIDDYTYPEZFDD))
1886  {
1887  v = 0;
1888  for (k = 1; k < biddyVariableTable.num; k++) {
1889  v = biddyVariableTable.table[v].prev;
1890  if (BiddyIsSmaller(v,BiddyV(f)) || (biddyVariableTable.table[v].selected == TRUE))
1891  {
1892  vname = Biddy_Managed_GetVariableName(MNG,v);
1893  Biddy_Managed_AddVariableByName(MNG2,vname);
1894  biddyVariableTable.table[v].selected = FALSE; /* deselect variable */
1895  }
1896  }
1897  }
1898 
1899  else if ((biddyManagerType2 == BIDDYTYPETZBDDC) || (biddyManagerType2 == BIDDYTYPETZBDD) ||
1900  (biddyManagerType2 == BIDDYTYPETZFDDC) || (biddyManagerType2 == BIDDYTYPETZFDD))
1901  {
1902  v = 0;
1903  for (k = 1; k < biddyVariableTable.num; k++) {
1904  v = biddyVariableTable.table[v].prev;
1905  if (biddyVariableTable.table[v].selected == TRUE) {
1906  vname = Biddy_Managed_GetVariableName(MNG,v);
1907  Biddy_Managed_AddVariableByName(MNG2,vname);
1908  biddyVariableTable.table[v].selected = FALSE; /* deselect variable */
1909  }
1910  }
1911  }
1912 
1913  else {
1914  fprintf(stderr,"Biddy_Managed_MinNodes: Unsupported BDD type!\n");
1915  }
1916 
1917  if (biddyVariableTable2.num == 1) {
1918  Biddy_ExitMNG(&MNG2);
1919  return 1;
1920  }
1921 
1922  f = BiddyCopy(MNG,MNG2,f); /* target manager is empty and has the same type */
1923 
1924  fidx = Biddy_Managed_AddTmpFormula(MNG2,(Biddy_String)"F",f);
1925 
1926  BiddySjtInit(MNG2);
1927 
1928  num = 0;
1929  first = TRUE;
1930  do {
1931  Biddy_Managed_FindFormula(MNG2,(Biddy_String)"F",&fidx,&f);
1932 
1933  /* use this to minimize the number of internal nodes */
1934  /*
1935  n = 0;
1936  Biddy_Managed_SelectNode(MNG2,biddyTerminal);
1937  BiddyNodeNumber(MNG2,f,&n);
1938  Biddy_Managed_DeselectAll(MNG2);
1939  */
1940 
1941  /* use this to minimize the number of all nodes */
1942 
1943  n = Biddy_Managed_CountNodes(MNG2,f);
1944 
1945 
1946  if (first || (n < num)) {
1947  num = n;
1948  }
1949 
1950  first = FALSE;
1951 
1952  } while(BiddySjtStep(MNG2));
1953 
1954  BiddySjtExit(MNG2);
1955  Biddy_ExitMNG(&MNG2);
1956 
1957  return num;
1958 }
1959 
1960 #ifdef __cplusplus
1961 }
1962 #endif
1963 
1964 /***************************************************************************/
1977 #ifdef __cplusplus
1978 extern "C" {
1979 #endif
1980 
1981 unsigned int
1983  Biddy_Manager MNG2;
1984  Biddy_Variable k,v;
1985  Biddy_String vname;
1986  unsigned int fidx;
1987  unsigned int n,num;
1988  Biddy_Boolean first;
1989 
1990  if (!MNG) MNG = biddyAnonymousManager;
1991 
1992  if (Biddy_IsNull(f)) return 0;
1993  if (f == biddyZero) return 1;
1994 
1995  num = Biddy_Managed_DependentVariableNumber(MNG,f,TRUE);
1996  if (num > 9) {
1997  printf("Biddy_Managed_MaxNodes: Function has to many variables (%u)!\n",num);
1998  for (k = 0; k < biddyVariableTable.num; k++) {
1999  biddyVariableTable.table[k].selected = FALSE; /* deselect variable */
2000  }
2001  return 0;
2002  }
2003 
2004  num = 0;
2006 
2007  /* COPY THE DOMAIN - DEPENDENT VARIABLES ONLY */
2008  /* the ordering of the new variable is determined in Biddy_InitMNG */
2009  /* FOR OBDDs AND OFDDs: new variable is added below (bottommore) all others */
2010  /* FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: new variable is added above (topmore) all others */
2011  /* FINAL ORDER FOR OBDDs AND OFDDs: [1] < [2] < ... < [size-1] < [0] */
2012  /* FINAL ORDER FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: [size-1] < [size-2] < ... < [1] < [0] */
2013  if ((biddyManagerType2 == BIDDYTYPEOBDDC) || (biddyManagerType2 == BIDDYTYPEOBDD) ||
2014  (biddyManagerType2 == BIDDYTYPEOFDDC) || (biddyManagerType2 == BIDDYTYPEOFDD))
2015  {
2016  v = Biddy_Managed_GetLowestVariable(MNG); /* lowest = topmost */
2017  for (k = 1; k < biddyVariableTable.num; k++) {
2018  if (biddyVariableTable.table[v].selected == TRUE) {
2019  vname = Biddy_Managed_GetVariableName(MNG,v);
2020  Biddy_Managed_AddVariableByName(MNG2,vname);
2021  biddyVariableTable.table[v].selected = FALSE; /* deselect variable */
2022  }
2023  v = biddyVariableTable.table[v].next;
2024  }
2025  }
2026 
2027  else if ((biddyManagerType2 == BIDDYTYPEZBDDC) || (biddyManagerType2 == BIDDYTYPEZBDD) ||
2028  (biddyManagerType2 == BIDDYTYPEZFDDC) || (biddyManagerType2 == BIDDYTYPEZFDD))
2029  {
2030  v = 0;
2031  for (k = 1; k < biddyVariableTable.num; k++) {
2032  v = biddyVariableTable.table[v].prev;
2033  if (BiddyIsSmaller(v,BiddyV(f)) || (biddyVariableTable.table[v].selected == TRUE))
2034  {
2035  vname = Biddy_Managed_GetVariableName(MNG,v);
2036  Biddy_Managed_AddVariableByName(MNG2,vname);
2037  biddyVariableTable.table[v].selected = FALSE; /* deselect variable */
2038  }
2039  }
2040  }
2041 
2042  else if ((biddyManagerType2 == BIDDYTYPETZBDDC) || (biddyManagerType2 == BIDDYTYPETZBDD) ||
2043  (biddyManagerType2 == BIDDYTYPETZFDDC) || (biddyManagerType2 == BIDDYTYPETZFDD))
2044  {
2045  v = 0;
2046  for (k = 1; k < biddyVariableTable.num; k++) {
2047  v = biddyVariableTable.table[v].prev;
2048  if (biddyVariableTable.table[v].selected == TRUE) {
2049  vname = Biddy_Managed_GetVariableName(MNG,v);
2050  Biddy_Managed_AddVariableByName(MNG2,vname);
2051  biddyVariableTable.table[v].selected = FALSE; /* deselect variable */
2052  }
2053  }
2054  }
2055 
2056  else {
2057  fprintf(stderr,"Biddy_Managed_MaxNodes: Unsupported BDD type!\n");
2058  }
2059 
2060  if (biddyVariableTable2.num == 1) {
2061  Biddy_ExitMNG(&MNG2);
2062  return 1;
2063  }
2064 
2065  f = BiddyCopy(MNG,MNG2,f); /* target manager is empty and has the same type */
2066 
2067  fidx = Biddy_Managed_AddTmpFormula(MNG2,(Biddy_String)"F",f);
2068 
2069  BiddySjtInit(MNG2);
2070 
2071  num = 0;
2072  first = TRUE;
2073  do {
2074  Biddy_Managed_FindFormula(MNG2,(Biddy_String)"F",&fidx,&f);
2075 
2076  /* use this to maximize the number of internal nodes */
2077  /*
2078  n = 0;
2079  Biddy_Managed_SelectNode(MNG2,biddyTerminal);
2080  BiddyNodeNumber(MNG2,f,&n);
2081  Biddy_Managed_DeselectAll(MNG2);
2082  */
2083 
2084  /* use this to minimize the number of all nodes */
2085 
2086  n = Biddy_Managed_CountNodes(MNG2,f);
2087 
2088 
2089  if (first || (n > num)) {
2090  num = n;
2091  }
2092 
2093  first = FALSE;
2094 
2095  } while(BiddySjtStep(MNG2));
2096 
2097  BiddySjtExit(MNG2);
2098  Biddy_ExitMNG(&MNG2);
2099 
2100  return num;
2101 }
2102 
2103 #ifdef __cplusplus
2104 }
2105 #endif
2106 
2107 /***************************************************************************/
2119 #ifdef __cplusplus
2120 extern "C" {
2121 #endif
2122 
2123 unsigned long long int
2125  Biddy_Variable v;
2126  unsigned i;
2127  BiddyCacheList *c;
2128  unsigned long long int n;
2129 
2130  if (!MNG) MNG = biddyAnonymousManager;
2131 
2132  n = 0;
2133 
2134  /* nodes */
2135  n += biddyNodeTable.generated * sizeof(BiddyNode);
2136 
2137  /* node table */
2138  n += sizeof(BiddyNodeTable) +
2139  biddyNodeTable.blocknumber * sizeof(BiddyNode *) +
2140  (biddyNodeTable.size+2) * sizeof(BiddyNode *);
2141 
2142  /* variable table */
2143  n += sizeof(BiddyVariableTable) +
2144  biddyVariableTable.size * sizeof(BiddyVariable);
2145  /* n += biddyVariableTable.size * sizeof(BiddyLookupVariable); */ /* currently not used */
2146  for (v=0; v<biddyVariableTable.num; v++) {
2147  if (biddyVariableTable.table[v].name) {
2148  n += strlen(biddyVariableTable.table[v].name) + 1;
2149  }
2150  }
2151 
2152  /* ordering table */
2153  n += sizeof(BiddyOrderingTable);
2154 
2155  /* formula table */
2156  n += sizeof(BiddyFormulaTable) +
2157  biddyFormulaTable.size * sizeof(BiddyFormula);
2158  if (biddyFormulaTable.deletedName) {
2159  n += strlen(biddyFormulaTable.deletedName) + 1;
2160  }
2161  for (i=0; i<biddyFormulaTable.size; i++) {
2162  if (biddyFormulaTable.table[i].name) {
2163  n += strlen(biddyFormulaTable.table[i].name) + 1;
2164  }
2165  }
2166 
2167  /* cache list*/
2168  c = biddyCacheList;
2169  while (c) {
2170  n += sizeof(BiddyCacheList);
2171  c = c->next;
2172  }
2173 
2174  /* OP cache */
2175  n += sizeof(BiddyOp3CacheTable) +
2176  (biddyOPCache.size+1) * sizeof(BiddyOp3Cache);
2177  n += sizeof(Biddy_Boolean); /* notusedyet */
2178  n += 4 * sizeof(unsigned long long int); /* counters */
2179 
2180  /* EA cache */
2181  n += sizeof(BiddyOp3CacheTable) +
2182  (biddyEACache.size+1) * sizeof(BiddyOp3Cache);
2183  n += sizeof(Biddy_Boolean); /* notusedyet */
2184  n += 4 * sizeof(unsigned long long int); /* counters */
2185 
2186  /* RC cache */
2187  n += sizeof(BiddyOp3CacheTable) +
2188  (biddyRCCache.size+1) * sizeof(BiddyOp3Cache);
2189  n += sizeof(Biddy_Boolean); /* notusedyet */
2190  n += 4 * sizeof(unsigned long long int); /* counters */
2191 
2192  /* REPLACE cache */
2193  n += sizeof(BiddyKeywordCacheTable) +
2194  (biddyReplaceCache.size+1) * sizeof(BiddyKeywordCache);
2195  n += (biddyReplaceCache.keywordNum) * sizeof(Biddy_String);
2196  n += (biddyReplaceCache.keywordNum) * sizeof(unsigned int);
2197  n += sizeof(Biddy_Boolean); /* notusedyet */
2198  n += 4 * sizeof(unsigned long long int); /* counters */
2199 
2200  return n;
2201 }
2202 
2203 #ifdef __cplusplus
2204 }
2205 #endif
2206 
2207 /***************************************************************************/
2216 #ifdef __cplusplus
2217 extern "C" {
2218 #endif
2219 
2220 void
2222 
2223  if (!MNG) MNG = biddyAnonymousManager;
2224 
2225  /* we have problems with passing stdout between mingw-based main and visual-studio-based dll */
2226  if (!f) f = stdout;
2227 
2228  fprintf(f,"**** System parameters ****\n");
2229  fprintf(f,"BDD TYPE: %s\n",Biddy_Managed_GetManagerName(MNG));
2230  fprintf(f,"UINTPTRSIZE = %u bits\n",(unsigned int) UINTPTRSIZE);
2231  fprintf(f,"sizeof(clock_t): %u bytes\n",(unsigned int)sizeof(clock_t));
2232  fprintf(f,"sizeof(BiddyNode *): %u bytes\n",(unsigned int)sizeof(BiddyNode *));
2233  fprintf(f,"sizeof(BiddyNode): %u bytes\n",(unsigned int)sizeof(BiddyNode));
2234  fprintf(f,"sizeof(BiddyVariable): %u bytes\n",(unsigned int)sizeof(BiddyVariable));
2235  fprintf(f,"sizeof(BiddyFormula): %u bytes\n",(unsigned int)sizeof(BiddyFormula));
2236  fprintf(f,"sizeof(BiddyOp3Cache): %u bytes\n",(unsigned int)sizeof(BiddyOp3Cache));
2237  fprintf(f,"sizeof(BiddyOrderingTable): %u bytes\n",(unsigned int)sizeof(BiddyOrderingTable));
2238  fprintf(f,"**** Biddy modifiable parameters ****\n");
2239  fprintf(f,"Limit for number of variables: %u\n",biddyVariableTable.size);
2240  fprintf(f,"Initial number of buckets in Node table: %u\n",biddyNodeTable.initsize+1);
2241  fprintf(f,"Number of nodes in the initial memory block: %u\n",biddyNodeTable.initblocksize);
2242  fprintf(f,"Initial OP cache size: %u\n",biddyOPCache.size);
2243  fprintf(f,"Initial EA cache size: %u\n",biddyEACache.size);
2244  fprintf(f,"Initial RC cache size: %u\n",biddyRCCache.size);
2245  fprintf(f,"Initial Replace cache size: %u\n",biddyReplaceCache.size);
2246  fprintf(f,"**** Biddy non-modifiable parameters ****\n");
2247 #ifdef MINGW
2248  fprintf(f, "Memory in use: %I64u bytes\n",Biddy_Managed_ReadMemoryInUse(MNG));
2249 #else
2250  fprintf(f, "Memory in use: %llu bytes\n",Biddy_Managed_ReadMemoryInUse(MNG));
2251 #endif
2252  fprintf(f,"Number of memory blocks: %u\n",biddyNodeTable.blocknumber);
2253  fprintf(f,"Number of nodes in the last memory block: %u\n",biddyNodeTable.blocksize);
2254  fprintf(f,"Number of variables: %u\n",biddyVariableTable.num);
2255  fprintf(f,"Number of formulae: %u\n",biddyFormulaTable.size);
2256  fprintf(f,"Peak number of BDD nodes: %u\n",biddyNodeTable.generated);
2257  fprintf(f,"Peak number of live BDD nodes: %u\n",biddyNodeTable.max);
2258  fprintf(f,"Number of live BDD nodes: %u\n",biddyNodeTable.num);
2259  fprintf(f,"Garbage collections so far: %u (node table resizing was used in %u of them)\n",biddyNodeTable.garbage,biddyNodeTable.nodetableresize);
2260 #ifdef BIDDYEXTENDEDSTATS_YES
2261 #ifdef MINGW
2262  fprintf(f,"Total number of obsolete nodes deleted: %I64u\n",Biddy_Managed_NodeTableGCObsoleteNumber(MNG));
2263 #else
2264  fprintf(f,"Total number of obsolete nodes deleted: %llu\n",Biddy_Managed_NodeTableGCObsoleteNumber(MNG));
2265 #endif
2266 #endif
2267  fprintf(f,"Total time for garbage collections so far: %.3fs\n",biddyNodeTable.gctime / (1.0 * CLOCKS_PER_SEC));
2268  fprintf(f,"Dynamic reorderings so far: %u\n",biddyNodeTable.sifting);
2269  fprintf(f,"Node swaps in dynamic reorderings: %u\n",biddyNodeTable.swap);
2270  fprintf(f,"Total time for dynamic reorderings so far: %.3fs\n",biddyNodeTable.drtime / (1.0 * CLOCKS_PER_SEC));
2271  fprintf(f,"**** Node Table stats ****\n");
2272  fprintf(f,"Number of buckets in Node table: %u\n",biddyNodeTable.size+1);
2273  fprintf(f,"Used buckets in Node table: %u (%.2f%%)\n",
2275  (100.0*Biddy_Managed_ListUsed(MNG)/(biddyNodeTable.size+1)));
2276  fprintf(f,"Max bucket's size in Node table: %u\n",Biddy_Managed_ListMaxLength(MNG));
2277  fprintf(f,"Avg bucket's size in Node table: %f\n",Biddy_Managed_ListAvgLength(MNG));
2278 #ifdef BIDDYEXTENDEDSTATS_YES
2279 #ifdef MINGW
2280  fprintf(f, "Number of ITE calls: %u (internal and recursive calls: %I64u)\n",biddyNodeTable.funite,biddyNodeTable.iterecursive);
2281  fprintf(f, "Number of AND or OR calls: %u (internal and recursive calls: %I64u)\n",biddyNodeTable.funandor,biddyNodeTable.andorrecursive);
2282  fprintf(f, "Number of XOR calls: %u (internal and recursive calls: %I64u)\n",biddyNodeTable.funxor,biddyNodeTable.xorrecursive);
2283  fprintf(f, "Number of node table FOA calls: %I64u\n",biddyNodeTable.foa);
2284  fprintf(f, "Number of node table insertions: %I64u\n",biddyNodeTable.add);
2285  fprintf(f, "Number of compared nodes: %I64u (%.2f per findNodeTable call)\n",
2286  biddyNodeTable.compare,
2287  biddyNodeTable.find ?
2288  (1.0*biddyNodeTable.compare/biddyNodeTable.find):0);
2289 #else
2290  fprintf(f, "Number of ITE calls: %u (internal and recursive calls: %llu)\n",biddyNodeTable.funite,biddyNodeTable.iterecursive);
2291  fprintf(f, "Number of AND and OR calls: %u (internal and recursive calls: %llu)\n",biddyNodeTable.funandor,biddyNodeTable.andorrecursive);
2292  fprintf(f, "Number of XOR calls: %u (internal and recursive calls: %llu)\n",biddyNodeTable.funxor,biddyNodeTable.xorrecursive);
2293  fprintf(f, "Number of node table FOA calls: %llu\n",biddyNodeTable.foa);
2294  fprintf(f, "Number of node table insertions: %llu\n",biddyNodeTable.add);
2295  fprintf(f, "Number of compared nodes: %llu (%.2f per findNodeTable call)\n",
2296  biddyNodeTable.compare,
2297  biddyNodeTable.find ?
2298  (1.0*biddyNodeTable.compare/biddyNodeTable.find):0);
2299 #endif
2300 #endif
2301  fprintf(f,"**** OP cache stats ****\n");
2302  fprintf(f,"Size of OP cache: %u\n",biddyOPCache.size);
2303 #ifdef MINGW
2304  fprintf(f, "Number of OP cache look-ups: %I64u\n",*(biddyOPCache.search));
2305  fprintf(f, "Number of OP cache hits: %I64u (%.2f%% of all calls)\n",
2306  *(biddyOPCache.find),
2307  *(biddyOPCache.search) ?
2308  (100.0*(*(biddyOPCache.find))/(*(biddyOPCache.search))):0);
2309 #ifdef BIDDYEXTENDEDSTATS_YES
2310  fprintf(f,"Number of OP cache insertions: %I64u (%.2f%% of all calls)\n",
2311  *(biddyOPCache.insert),
2312  *(biddyOPCache.search) ?
2313  (100.0*(*(biddyOPCache.insert))/(*(biddyOPCache.search))):0);
2314  fprintf(f, "Number of OP cache collisions: %I64u (%.2f%% of all insertions, %.2f%% of all calls)\n",
2315  *(biddyOPCache.overwrite),
2316  (*(biddyOPCache.insert)) ?
2317  (100.0*(*(biddyOPCache.overwrite))/(*(biddyOPCache.insert))):0,
2318  *(biddyOPCache.search) ?
2319  (100.0*(*(biddyOPCache.overwrite))/(*(biddyOPCache.search))):0);
2320 #endif
2321 #else
2322  fprintf(f, "Number of OP cache look-ups: %llu\n",*(biddyOPCache.search));
2323  fprintf(f, "Number of OP cache hits: %llu (%.2f%% of all calls)\n",
2324  *(biddyOPCache.find),
2325  *(biddyOPCache.search) ?
2326  (100.0*(*(biddyOPCache.find))/(*(biddyOPCache.search))):0);
2327 #ifdef BIDDYEXTENDEDSTATS_YES
2328  fprintf(f,"Number of OP cache insertions: %llu (%.2f%% of all calls)\n",
2329  *(biddyOPCache.insert),
2330  *(biddyOPCache.search) ?
2331  (100.0*(*(biddyOPCache.insert))/(*(biddyOPCache.search))):0);
2332  fprintf(f, "Number of OP cache collisions: %llu (%.2f%% of all insertions, %.2f%% of all calls)\n",
2333  *(biddyOPCache.overwrite),
2334  (*(biddyOPCache.insert)) ?
2335  (100.0*(*(biddyOPCache.overwrite))/(*(biddyOPCache.insert))):0,
2336  *(biddyOPCache.search) ?
2337  (100.0*(*(biddyOPCache.overwrite))/(*(biddyOPCache.search))):0);
2338 #endif
2339 #endif
2340  fprintf(f,"**** EA cache stats ****\n");
2341  fprintf(f,"Size of EA cache: %u\n",biddyEACache.size);
2342 #ifdef MINGW
2343  fprintf(f, "Number of EA cache look-ups: %I64u\n",*(biddyEACache.search));
2344  fprintf(f, "Number of EA cache hits: %I64u (%.2f%% of all calls)\n",
2345  *(biddyEACache.find),
2346  (*(biddyEACache.search)) ?
2347  (100.0*(*(biddyEACache.find))/(*(biddyEACache.search))):0);
2348 #ifdef BIDDYEXTENDEDSTATS_YES
2349  fprintf(f,"Number of EA cache insertions: %I64u (%.2f%% of all calls)\n",
2350  *(biddyEACache.insert),
2351  (*(biddyEACache.search)) ?
2352  (100.0*(*(biddyEACache.insert))/(*(biddyEACache.search))):0);
2353  fprintf(f, "Number of EA cache collisions: %I64u (%.2f%% of all insertions, %.2f%% of all calls)\n",
2354  *(biddyEACache.overwrite),
2355  (*(biddyEACache.insert)) ?
2356  (100.0*(*(biddyEACache.overwrite))/(*(biddyEACache.insert))):0,
2357  (*(biddyEACache.search)) ?
2358  (100.0*(*(biddyEACache.overwrite))/(*(biddyEACache.search))):0);
2359 #endif
2360 #else
2361  fprintf(f, "Number of EA cache look-ups: %llu\n",*(biddyEACache.search));
2362  fprintf(f, "Number of EA cache hits: %llu (%.2f%% of all calls)\n",
2363  *(biddyEACache.find),
2364  (*(biddyEACache.search)) ?
2365  (100.0*(*(biddyEACache.find))/(*(biddyEACache.search))):0);
2366 #ifdef BIDDYEXTENDEDSTATS_YES
2367  fprintf(f,"Number of EA cache insertions: %llu (%.2f%% of all calls)\n",
2368  *(biddyEACache.insert),
2369  (*(biddyEACache.search)) ?
2370  (100.0*(*(biddyEACache.insert))/(*(biddyEACache.search))):0);
2371  fprintf(f, "Number of EA cache collisions: %llu (%.2f%% of all insertions, %.2f%% of all calls)\n",
2372  *(biddyEACache.overwrite),
2373  (*(biddyEACache.insert)) ?
2374  (100.0*(*(biddyEACache.overwrite))/(*(biddyEACache.insert))):0,
2375  (*(biddyEACache.search)) ?
2376  (100.0*(*(biddyEACache.overwrite))/(*(biddyEACache.search))):0);
2377 #endif
2378 #endif
2379  fprintf(f,"**** RC cache stats ****\n");
2380  fprintf(f,"Size of RC cache: %u\n",biddyRCCache.size);
2381 #ifdef MINGW
2382  fprintf(f, "Number of RC cache look-ups: %I64u\n",*(biddyRCCache.search));
2383  fprintf(f, "Number of RC cache hits: %I64u (%.2f%% of all calls)\n",
2384  *(biddyRCCache.find),
2385  (*(biddyRCCache.search)) ?
2386  (100.0*(*(biddyRCCache.find))/(*(biddyRCCache.search))):0);
2387 #ifdef BIDDYEXTENDEDSTATS_YES
2388  fprintf(f,"Number of RC cache insertions: %I64u (%.2f%% of all calls)\n",
2389  *(biddyRCCache.insert),
2390  (*(biddyRCCache.search)) ?
2391  (100.0*(*(biddyRCCache.insert))/(*(biddyRCCache.search))):0);
2392  fprintf(f, "Number of RC cache collisions: %I64u (%.2f%% of all insertions, %.2f%% of all calls)\n",
2393  *(biddyRCCache.overwrite),
2394  (*(biddyRCCache.insert)) ?
2395  (100.0*(*(biddyRCCache.overwrite))/(*(biddyRCCache.insert))):0,
2396  (*(biddyRCCache.search)) ?
2397  (100.0*(*(biddyRCCache.overwrite))/(*(biddyRCCache.search))):0);
2398 #endif
2399 #else
2400  fprintf(f, "Number of RC cache look-ups: %llu\n",*(biddyRCCache.search));
2401  fprintf(f, "Number of RC cache hits: %llu (%.2f%% of all calls)\n",
2402  *(biddyRCCache.find),
2403  (*(biddyRCCache.search)) ?
2404  (100.0*(*(biddyRCCache.find))/(*(biddyRCCache.search))):0);
2405 #ifdef BIDDYEXTENDEDSTATS_YES
2406  fprintf(f,"Number of RC cache insertions: %llu (%.2f%% of all calls)\n",
2407  *(biddyRCCache.insert),
2408  (*(biddyRCCache.search)) ?
2409  (100.0*(*(biddyRCCache.insert))/(*(biddyRCCache.search))):0);
2410  fprintf(f, "Number of RC cache collisions: %llu (%.2f%% of all insertions, %.2f%% of all calls)\n",
2411  *(biddyRCCache.overwrite),
2412  (*(biddyRCCache.insert)) ?
2413  (100.0*(*(biddyRCCache.overwrite))/(*(biddyRCCache.insert))):0,
2414  (*(biddyRCCache.search)) ?
2415  (100.0*(*(biddyRCCache.overwrite))/(*(biddyRCCache.search))):0);
2416 #endif
2417 #endif
2418  fprintf(f,"**** Replace cache stats ****\n");
2419  fprintf(f,"Size of Replace cache: %u\n",biddyReplaceCache.size);
2420 #ifdef MINGW
2421  fprintf(f, "Number of Replace cache look-ups: %I64u\n",*(biddyReplaceCache.search));
2422  fprintf(f, "Number of Replace cache hits: %I64u (%.2f%% of all calls)\n",
2423  *(biddyReplaceCache.find),
2424  (*(biddyReplaceCache.search)) ?
2425  (100.0*(*(biddyReplaceCache.find))/(*(biddyReplaceCache.search))):0);
2426 #ifdef BIDDYEXTENDEDSTATS_YES
2427  fprintf(f,"Number of Replace cache insertions: %I64u (%.2f%% of all calls)\n",
2428  *(biddyReplaceCache.insert),
2429  (*(biddyReplaceCache.search)) ?
2430  (100.0*(*(biddyReplaceCache.insert))/(*(biddyReplaceCache.search))):0);
2431  fprintf(f, "Number of Replace cache collisions: %I64u (%.2f%% of all insertions, %.2f%% of all calls)\n",
2432  *(biddyReplaceCache.overwrite),
2433  (*(biddyReplaceCache.insert)) ?
2434  (100.0*(*(biddyReplaceCache.overwrite))/(*(biddyReplaceCache.insert))):0,
2435  (*(biddyReplaceCache.search)) ?
2436  (100.0*(*(biddyReplaceCache.overwrite))/(*(biddyReplaceCache.search))):0);
2437 #endif
2438 #else
2439  fprintf(f, "Number of Replace cache look-ups: %llu\n",*(biddyReplaceCache.search));
2440  fprintf(f, "Number of Replace cache hits: %llu (%.2f%% of all calls)\n",
2441  *(biddyReplaceCache.find),
2442  (*(biddyReplaceCache.search)) ?
2443  (100.0*(*(biddyReplaceCache.find))/(*(biddyReplaceCache.search))):0);
2444 #ifdef BIDDYEXTENDEDSTATS_YES
2445  fprintf(f,"Number of Replace cache insertions: %llu (%.2f%% of all calls)\n",
2446  *(biddyReplaceCache.insert),
2447  (*(biddyReplaceCache.search)) ?
2448  (100.0*(*(biddyReplaceCache.insert))/(*(biddyReplaceCache.search))):0);
2449  fprintf(f, "Number of Replace cache collisions: %llu (%.2f%% of all insertions, %.2f%% of all calls)\n",
2450  *(biddyReplaceCache.overwrite),
2451  (*(biddyReplaceCache.insert)) ?
2452  (100.0*(*(biddyReplaceCache.overwrite))/(*(biddyReplaceCache.insert))):0,
2453  (*(biddyReplaceCache.search)) ?
2454  (100.0*(*(biddyReplaceCache.overwrite))/(*(biddyReplaceCache.search))):0);
2455 #endif
2456 #endif
2457  fprintf(f,"**** END OF STATS ****\n");
2458 }
2459 
2460 #ifdef __cplusplus
2461 }
2462 #endif
2463 
2464 /*----------------------------------------------------------------------------*/
2465 /* Definition of internal functions */
2466 /*----------------------------------------------------------------------------*/
2467 
2468 /*******************************************************************************
2469 \brief Function BiddyNodeNumber.
2470 
2471 ### Description
2472 ### Side effects
2473  Terminal node must be selected! Function will select all other nodes.
2474 ### More info
2475 *******************************************************************************/
2476 
2477 void
2478 BiddyNodeNumber(Biddy_Manager MNG, Biddy_Edge f, unsigned int *n)
2479 {
2480  if (!Biddy_Managed_IsSelected(MNG,f)) {
2481  Biddy_Managed_SelectNode(MNG,f);
2482  (*n)++;
2483  BiddyNodeNumber(MNG,BiddyE(f),n);
2484  BiddyNodeNumber(MNG,BiddyT(f),n);
2485  }
2486 }
2487 
2488 
2489 /*******************************************************************************
2490 \brief Function BiddyComplementedEdgeNumber.
2491 
2492 ### Description
2493 ### Side effects
2494  Terminal node must be selected! Function will select all other nodes.
2495 ### More info
2496 *******************************************************************************/
2497 
2498 void
2499 BiddyComplementedEdgeNumber(Biddy_Manager MNG, Biddy_Edge f, unsigned int *n)
2500 {
2501  if (Biddy_GetMark(f)) (*n)++;
2502  if (!Biddy_Managed_IsSelected(MNG,f)) {
2503  Biddy_Managed_SelectNode(MNG,f);
2504  BiddyComplementedEdgeNumber(MNG,BiddyE(f),n);
2505  BiddyComplementedEdgeNumber(MNG,BiddyT(f),n);
2506  }
2507 }
2508 
2509 /*******************************************************************************
2510 \brief Function BiddyNodeVarNumber.
2511 
2512 ### Description
2513  Count number of nodes and number of dependent variables.
2514  For OBDDs, the number of variables existing in the graph is the same as
2515  the number of dependent variables. For ZBDDs and TZBDDs, this is not true.
2516 ### Side effects
2517  Terminal node must be selected! Function will select all other nodes.
2518  Function will select all dependent variables.
2519  For ZBDDs, variables above the top variable (which are always
2520  all dependent) are not counted and not selected!
2521  For TZBDDs, variables above the top variable (those equal or greater than
2522  the top tag are all dependent) are not counted and not selected!
2523 ### More info
2524 *******************************************************************************/
2525 
2526 void
2527 BiddyNodeVarNumber(Biddy_Manager MNG, Biddy_Edge f, unsigned int *n)
2528 {
2529  Biddy_Edge e,t;
2530  Biddy_Variable v,w;
2531 
2532 
2533  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD))
2534  {
2535  if (Biddy_Managed_IsSelected(MNG,f)) {
2536  /* ALREADY VISITED */
2537  return;
2538  } else {
2539  assert( BiddyIsSmaller(BiddyV(f),BiddyV(BiddyE(f))) );
2540  assert( BiddyIsSmaller(BiddyV(f),BiddyV(BiddyT(f))) );
2541  Biddy_Managed_SelectNode(MNG,f);
2542  (*n)++;
2543  v = BiddyV(f);
2544  e = BiddyE(f); /* here, mark is not important */
2545  t = BiddyT(f); /* here, mark is not important */
2546  biddyVariableTable.table[v].selected = TRUE;
2547  BiddyNodeVarNumber(MNG,e,n);
2548  BiddyNodeVarNumber(MNG,t,n);
2549  }
2550  }
2551 
2552  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD))
2553  {
2554  if (Biddy_IsTerminal(f)) return;
2555  if (Biddy_Managed_IsSelected(MNG,f)) {
2556  if (BiddyIsSelectedNP(f)) {
2557  /* ALREADY VISITED WITH THE SAME MARK */
2558  return;
2559  } else {
2560  /* ALREADY VISITED, BUT WITH DIFFERENT MARK */
2561  BiddySelectNP(f);
2562  }
2563  } else {
2564  /* NOT VISITED */
2565  assert( BiddyIsSmaller(BiddyV(f),BiddyV(BiddyE(f))) );
2566  assert( BiddyIsSmaller(BiddyV(f),BiddyV(BiddyT(f))) );
2567  Biddy_Managed_SelectNode(MNG,f);
2568  BiddySelectNP(f);
2569  (*n)++;
2570  }
2571  v = BiddyV(f);
2572  e = Biddy_Managed_TransferMark(MNG,BiddyE(f),Biddy_GetMark(f),TRUE); /* TRUE = left */
2573  t = Biddy_Managed_TransferMark(MNG,BiddyT(f),Biddy_GetMark(f),FALSE); /* FALSE = right */
2574  if (e != t) {
2575  biddyVariableTable.table[v].selected = TRUE;
2576  }
2577  v = biddyVariableTable.table[v].next;
2578  w = BiddyV(t); /* for ZBDD, t cannot be biddyZero */
2579  if ((e != biddyZero) && BiddyIsSmaller(w,BiddyV(e))) w = BiddyV(e);
2580  while ((v != 0) && (v != w)) {
2581  biddyVariableTable.table[v].selected = TRUE;
2582  v = biddyVariableTable.table[v].next;
2583  }
2584  BiddyNodeVarNumber(MNG,e,n);
2585  BiddyNodeVarNumber(MNG,t,n);
2586  }
2587 
2588  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
2589  {
2590  if (Biddy_Managed_IsSelected(MNG,f)) {
2591  /* ALREADY VISITED */
2592  return;
2593  } else {
2594 
2595  assert( (Biddy_GetTag(f) == BiddyV(f)) || BiddyIsSmaller(Biddy_GetTag(f),BiddyV(f)) );
2596  assert( BiddyIsSmaller(BiddyV(f),BiddyV(BiddyE(f))) );
2597  assert( BiddyIsSmaller(BiddyV(f),BiddyV(BiddyT(f))) );
2598  assert( (Biddy_GetTag(BiddyE(f)) == BiddyV(BiddyE(f))) || BiddyIsSmaller(Biddy_GetTag(BiddyE(f)),BiddyV(BiddyE(f))) );
2599  assert( (Biddy_GetTag(BiddyT(f)) == BiddyV(BiddyT(f))) || BiddyIsSmaller(Biddy_GetTag(BiddyT(f)),BiddyV(BiddyT(f))) );
2600 
2601  /* DEBUGGING */
2602  /*
2603  if (BiddyIsSmaller(BiddyV(f),Biddy_GetTag(f)) ||
2604  !BiddyIsSmaller(BiddyV(f),BiddyV(BiddyE(f))) ||
2605  !BiddyIsSmaller(BiddyV(f),BiddyV(BiddyT(f))))
2606  {
2607  printf("ERROR:");
2608  printf("<\"%s\",",Biddy_Managed_GetTopVariableName(MNG,f));
2609  if (!Biddy_IsNull(BiddyE(f)) && Biddy_GetMark(BiddyE(f))) printf("*");
2610  if (Biddy_IsNull(BiddyE(f))) printf("NULL,");
2611  else printf("<\"%s\">\"%s\",",Biddy_Managed_GetVariableName(MNG,Biddy_GetTag(BiddyE(f))),Biddy_Managed_GetTopVariableName(MNG,BiddyE(f)));
2612  if (!Biddy_IsNull(BiddyT(f)) && Biddy_GetMark(BiddyT(f))) printf("*");
2613  if (Biddy_IsNull(BiddyT(f))) printf("NULL>");
2614  else printf("<\"%s\">\"%s\">",Biddy_Managed_GetVariableName(MNG,Biddy_GetTag(BiddyT(f))),Biddy_Managed_GetTopVariableName(MNG,BiddyT(f)));
2615  printf("@%u",BiddyN(f)->expiry);
2616  printf("\n");
2617  }
2618  assert( (Biddy_GetTag(f) == BiddyV(f)) || BiddyIsSmaller(Biddy_GetTag(f),BiddyV(f)) );
2619  assert( BiddyIsSmaller(BiddyV(f),BiddyV(BiddyE(f))) );
2620  assert( BiddyIsSmaller(BiddyV(f),BiddyV(BiddyT(f))) );
2621  */
2622 
2623  Biddy_Managed_SelectNode(MNG,f);
2624  (*n)++;
2625  v = BiddyV(f);
2626  e = BiddyE(f); /* marks are not used */
2627  t = BiddyT(f); /* marks are not used */
2628  if (e != t) {
2629  biddyVariableTable.table[v].selected = TRUE;
2630  }
2631 
2632  /* DEBUGGING */
2633  /*
2634  if (BiddyIsSmaller(BiddyV(e),Biddy_GetTag(e))) {
2635  printf("ERROR:");
2636  printf("<\"%s\",",Biddy_Managed_GetTopVariableName(MNG,f));
2637  if (!Biddy_IsNull(e) && Biddy_GetMark(e)) printf("*");
2638  if (Biddy_IsNull(e)) printf("NULL,");
2639  else printf("<\"%s\">\"%s\",",Biddy_Managed_GetVariableName(MNG,Biddy_GetTag(e)),Biddy_Managed_GetTopVariableName(MNG,e));
2640  if (!Biddy_IsNull(t) && Biddy_GetMark(t)) printf("*");
2641  if (Biddy_IsNull(t)) printf("NULL>");
2642  else printf("<\"%s\">\"%s\">",Biddy_Managed_GetVariableName(MNG,Biddy_GetTag(t)),Biddy_Managed_GetTopVariableName(MNG,t));
2643  printf("@%u",BiddyN(f)->expiry);
2644  printf("\n");
2645  }
2646  assert ( (Biddy_GetTag(e) == BiddyV(e)) || BiddyIsSmaller(Biddy_GetTag(e),BiddyV(e)) );
2647  */
2648 
2649  w = Biddy_GetTag(e);
2650  while (w != BiddyV(e)) {
2651  biddyVariableTable.table[w].selected = TRUE;
2652  w = biddyVariableTable.table[w].next;
2653  }
2654 
2655  /* DEBUGGING */
2656  /*
2657  if (BiddyIsSmaller(BiddyV(t),Biddy_GetTag(t))) {
2658  printf("ERROR:");
2659  printf("<\"%s\",",Biddy_Managed_GetTopVariableName(MNG,f));
2660  if (!Biddy_IsNull(e) && Biddy_GetMark(e)) printf("*");
2661  if (Biddy_IsNull(e)) printf("NULL,");
2662  else printf("<\"%s\">\"%s\",",Biddy_Managed_GetVariableName(MNG,Biddy_GetTag(e)),Biddy_Managed_GetTopVariableName(MNG,e));
2663  if (!Biddy_IsNull(t) && Biddy_GetMark(t)) printf("*");
2664  if (Biddy_IsNull(t)) printf("NULL>");
2665  else printf("<\"%s\">\"%s\">",Biddy_Managed_GetVariableName(MNG,Biddy_GetTag(t)),Biddy_Managed_GetTopVariableName(MNG,t));
2666  printf("@%u",BiddyN(f)->expiry);
2667  printf("\n");
2668  }
2669  assert ( (Biddy_GetTag(t) == BiddyV(t)) || BiddyIsSmaller(Biddy_GetTag(t),BiddyV(t)) );
2670  */
2671 
2672  w = Biddy_GetTag(t);
2673  while (w != BiddyV(t)) {
2674  biddyVariableTable.table[w].selected = TRUE;
2675  w = biddyVariableTable.table[w].next;
2676  }
2677  BiddyNodeVarNumber(MNG,e,n);
2678  BiddyNodeVarNumber(MNG,t,n);
2679  }
2680  }
2681 
2682  else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
2683  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
2684  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
2685  {
2686  fprintf(stderr,"BiddyNodeVarNumber: this BDD type is not supported, yet!\n");
2687  return;
2688  }
2689 
2690  else {
2691  fprintf(stderr,"BiddyNodeVarNumber: Unsupported BDD type!\n");
2692  return;
2693  }
2694 
2695 }
2696 
2697 /*----------------------------------------------------------------------------*/
2698 /* Definition of static functions */
2699 /*----------------------------------------------------------------------------*/
2700 
2701 /*******************************************************************************
2702 \brief Function MaxLevel.
2703 
2704 ### Description
2705 ### Side effects
2706 ### More info
2707 *******************************************************************************/
2708 
2709 static void
2710 MaxLevel(Biddy_Edge f, unsigned int *max, unsigned int i)
2711 {
2712  i++;
2713  if (i > *max) *max = i;
2714  if (BiddyE(f) == BiddyT(f)) {
2715  if (!Biddy_IsNull(BiddyE(f))) MaxLevel(BiddyE(f),max,i);
2716  } else {
2717  if (!Biddy_IsNull(BiddyE(f))) MaxLevel(BiddyE(f),max,i);
2718  if (!Biddy_IsNull(BiddyT(f))) MaxLevel(BiddyT(f),max,i);
2719  }
2720 }
2721 
2722 /*******************************************************************************
2723 \brief Function AvgLevel.
2724 
2725 ### Description
2726 ### Side effects
2727  The result may not be compatible with your definition of Average Level
2728  for DAG. The result is especially problematic if there exists a node with
2729  two equal descendants (e.g for ZBDDs and TZBDDs).
2730 ### More info
2731 *******************************************************************************/
2732 
2733 static void
2734 AvgLevel(Biddy_Edge f, float *sum, unsigned int *n, unsigned int i)
2735 {
2736  i++;
2737  (*n)++;
2738  (*sum) = (*sum) + i;
2739  if (BiddyE(f) == BiddyT(f)) {
2740  if (!Biddy_IsNull(BiddyE(f))) AvgLevel(BiddyE(f),sum,n,i);
2741  } else {
2742  if (!Biddy_IsNull(BiddyE(f))) AvgLevel(BiddyE(f),sum,n,i);
2743  if (!Biddy_IsNull(BiddyT(f))) AvgLevel(BiddyT(f),sum,n,i);
2744  }
2745 }
2746 
2747 /*******************************************************************************
2748 \brief Function pathCount.
2749 
2750 ### Description
2751 ### Side effects
2752  Function will select all nodes except terminal node.
2753  TO DO: implement this using GNU Multiple Precision Arithmetic Library (GMP).
2754 ### More info
2755 *******************************************************************************/
2756 
2757 static void
2758 pathCount(Biddy_Manager MNG, Biddy_Edge f, unsigned long long int *c1,
2759  unsigned long long int *c0, Biddy_Boolean *leftmost)
2760 {
2761  unsigned long long int r1,r0;
2762 
2763  assert( f != NULL );
2764 
2765  assert((
2766  (biddyManagerType == BIDDYTYPEOBDD) ||
2767  (biddyManagerType == BIDDYTYPEOBDDC) ||
2768  (biddyManagerType == BIDDYTYPEZBDD) ||
2769  (biddyManagerType == BIDDYTYPEZBDDC) ||
2770  (biddyManagerType == BIDDYTYPETZBDD)
2771  ));
2772 
2773  /* DEBUGGING */
2774  /*
2775  printf("pathCount: f = %s (%p), c1 = %llu, c0 = %llu\n",Biddy_Managed_GetTopVariableName(MNG,f),f,*c1,*c0);
2776  */
2777 
2778  /* For OBDDs, c1 is number of ones, c0 is number of zeros, leftmost is not used */
2779  /* For ZBDDs, c1 is number of ones, c0 is not used, leftmost is the leftmost value */
2780  /* For TZBDDs, c1 is number of ones, c0 is not used, leftmost is not used */
2781  if (f == biddyZero) {
2782  *c1 = 0;
2783  *c0 = 1;
2784  *leftmost = FALSE;
2785  return;
2786  }
2787  if (Biddy_IsTerminal(f)) {
2788  *c1 = 1;
2789  *c0 = 0;
2790  *leftmost = TRUE;
2791  return;
2792  }
2793 
2794  if (Biddy_Managed_IsSelected(MNG,f)) {
2795  /* ALREADY VISITED */
2796  if (Biddy_GetMark(f)) {
2797  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2798  *c1 = BiddyGetPath0Count(f); /* positive edge is stored but actual edge is returned */
2799  *c0 = BiddyGetPath1Count(f); /* positive edge is stored but actual edge is returned */
2800  }
2801  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2802  *c1 = BiddyGetPath1Count(f); /* positive edge is stored */
2803  *leftmost = !(BiddyGetLeftmost(f)); /* actual edge is returned */
2804  if (*leftmost) {
2805  (*c1)++; /* actual edge is returned */
2806  } else {
2807  (*c1)--; /* actual edge is returned */
2808  }
2809  }
2810  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
2811  /* COMPLEMENTED EDGES ARE NOT USED FOR TZBDDs */
2812  }
2813  } else {
2814  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2815  *c1 = BiddyGetPath1Count(f);
2816  *c0 = BiddyGetPath0Count(f);
2817  }
2818  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2819  *c1 = BiddyGetPath1Count(f);
2820  *leftmost = BiddyGetLeftmost(f);
2821  }
2822  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
2823  *c1 = BiddyGetPath1Count(f);
2824  }
2825  }
2826  return;
2827  }
2828 
2829  /* NOT VISITED, YET */
2830  Biddy_Managed_SelectNode(MNG,f);
2831 
2832  /* COUNT PATHS FOR BOTH SUCCESSORS */
2833  /* because of parameter leftmost it is important to calculate BiddyT first! */
2834  pathCount(MNG,BiddyT(f),c1,c0,leftmost);
2835  pathCount(MNG,BiddyE(f),&r1,&r0,leftmost);
2836  *c1 += r1;
2837  *c0 += r0;
2838 
2839  /* STORE PATHS INTO LOCALINFO */
2840  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2841  BiddySetPath1Count(f,*c1); /* positive edge is stored */
2842  BiddySetPath0Count(f,*c0); /* positive edge is stored */
2843  if (Biddy_GetMark(f)) {
2844  *c1 = BiddyGetPath0Count(f); /* actual edge is returned */
2845  *c0 = BiddyGetPath1Count(f); /* actual edge is returned */
2846  }
2847  }
2848  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2849  BiddySetPath1Count(f,*c1); /* positive edge is stored */
2850  BiddySetLeftmost(f,*leftmost); /* positive edge is stored */
2851  if (Biddy_GetMark(f)) {
2852  *leftmost = !(*leftmost); /* actual edge is returned */
2853  if (*leftmost) {
2854  (*c1)++; /* actual edge is returned */
2855  } else {
2856  (*c1)--; /* actual edge is returned */
2857  }
2858  }
2859  }
2860  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
2861  BiddySetPath1Count(f,*c1);
2862  }
2863 
2864  /* DEBUGGING */
2865  /*
2866  printf("pathCount finished, results returned: c1=%llu, c0=%llu\n",*c1,*c0);
2867  */
2868 
2869  return;
2870 }
2871 
2872 /*******************************************************************************
2873 \brief Function mintermCount.
2874 
2875 ### Description
2876 ### Side effects
2877  We are using GNU Multiple Precision Arithmetic Library (GMP).
2878 ### More info
2879 *******************************************************************************/
2880 
2881 static void
2882 mintermCount(Biddy_Manager MNG, Biddy_Edge f, mpz_t max, mpz_t result,
2883  Biddy_Boolean *leftmost)
2884 {
2885  mpz_t countE,countT;
2886  Biddy_Variable v;
2887 
2888  assert((
2889  (biddyManagerType == BIDDYTYPEOBDD) ||
2890  (biddyManagerType == BIDDYTYPEOBDDC) ||
2891  (biddyManagerType == BIDDYTYPEZBDD) ||
2892  (biddyManagerType == BIDDYTYPEZBDDC) ||
2893  (biddyManagerType == BIDDYTYPETZBDD)
2894  ));
2895 
2896  /* For OBDD and TZBDD, leftmost is not used */
2897  /* For ZBDD, max is not used */
2898  if (f == biddyZero) {
2899  mpz_set_ui(result,0);
2900  *leftmost = FALSE;
2901  return;
2902  }
2903  if (Biddy_IsTerminal(f)) {
2904  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2905  mpz_set(result,max);
2906  }
2907  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2908  mpz_set_ui(result,1);
2909  }
2910  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
2911  mpz_set(result,max);
2912  v = BiddyV(f);
2913  while (v != Biddy_GetTag(f)) {
2914  mpz_divexact_ui(result,result,2); /* actual edge is returned */
2915  v = biddyVariableTable.table[v].prev;
2916  }
2917  }
2918  *leftmost = TRUE;
2919  return;
2920  }
2921 
2922  if (Biddy_Managed_IsSelected(MNG,f)) {
2923  /* ALREADY VISITED */
2924  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2925  BiddyGetMintermCount(f,result); /* positive edge is stored */
2926  if (Biddy_GetMark(f)) {
2927  mpz_sub(result,max,result); /* actual edge is returned */
2928  }
2929  }
2930  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2931  BiddyGetMintermCount(f,result); /* positive edge is stored */
2932  *leftmost = BiddyGetLeftmost(f); /* positive edge is stored */
2933  if (Biddy_GetMark(f)) {
2934  *leftmost = !(*leftmost); /* actual edge is returned */
2935  if (*leftmost) {
2936  mpz_add_ui(result,result,1); /* actual edge is returned */
2937  } else {
2938  mpz_sub_ui(result,result,1); /* actual edge is returned */
2939  }
2940  }
2941  }
2942  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
2943  BiddyGetMintermCount(f,result); /* untagged edge is stored */
2944  v = BiddyV(f);
2945  while (v != Biddy_GetTag(f)) {
2946  mpz_divexact_ui(result,result,2);
2947  v = biddyVariableTable.table[v].prev;
2948  }
2949  }
2950  return;
2951  }
2952 
2953  /* NOT VISITED, YET */
2954  Biddy_Managed_SelectNode(MNG,f);
2955 
2956  mpz_init(countE);
2957  mpz_init(countT);
2958 
2959  /* because of parameter leftmost it is important to calculate countT first! */
2960  mintermCount(MNG,BiddyT(f),max,countT,leftmost);
2961  mintermCount(MNG,BiddyE(f),max,countE,leftmost);
2962 
2963  mpz_add(result,countE,countT);
2964 
2965  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2966  mpz_divexact_ui(result,result,2);
2967  BiddySetMintermCount(f,result); /* positive edge is stored */
2968  if (Biddy_GetMark(f)) {
2969  mpz_sub(result,max,result); /* actual edge is returned */
2970  }
2971  }
2972  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2973  BiddySetMintermCount(f,result); /* positive edge is stored */
2974  BiddySetLeftmost(f,*leftmost); /* positive edge is stored */
2975  if (Biddy_GetMark(f)) {
2976  *leftmost = !(*leftmost); /* actual edge is returned */
2977  if (*leftmost) {
2978  mpz_add_ui(result,result,1); /* actual edge is returned */
2979  } else {
2980  mpz_sub_ui(result,result,1); /* actual edge is returned */
2981  }
2982  }
2983  }
2984  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
2985  mpz_divexact_ui(result,result,2);
2986  BiddySetMintermCount(f,result); /* untagged edge is stored */
2987  v = BiddyV(f);
2988  while (v != Biddy_GetTag(f)) {
2989  mpz_divexact_ui(result,result,2); /* actual edge is returned */
2990  v = biddyVariableTable.table[v].prev;
2991  }
2992  }
2993 
2994  mpz_clear(countE);
2995  mpz_clear(countT);
2996 }
2997 
2998 /*******************************************************************************
2999 \brief Function nodePlainNumber.
3000 
3001 ### Description
3002 ### Side effects
3003 ### More info
3004 *******************************************************************************/
3005 
3006 static unsigned int
3007 nodePlainNumber(Biddy_Manager MNG, Biddy_Edge f)
3008 {
3009  unsigned int n;
3010 
3011  assert( f != NULL );
3012 
3013  assert((
3014  (biddyManagerType == BIDDYTYPEOBDDC) ||
3015  (biddyManagerType == BIDDYTYPEZBDDC)
3016  ));
3017 
3018  /* DEBUGGING */
3019  /*
3020  printf("nodePlainNumber: f = %s (%p)\n",Biddy_Managed_GetTopVariableName(MNG,f),f);
3021  */
3022 
3023  if (Biddy_IsTerminal(f)) return 0;
3024  if (Biddy_Managed_IsSelected(MNG,f)) {
3025  if (BiddyIsSelectedNP(f)) {
3026  /* ALREADY VISITED */
3027  return 0;
3028  } else {
3029  /* MARK IS INVERTED */
3030  /* COUNTING MUST BE REPEATED */
3031  /* How to calculate plain number of the negated function from the existing info? */
3032  /* This seems to be impossible for all BDD types. */
3033  }
3034  }
3035 
3036  Biddy_Managed_SelectNode(MNG,f);
3037  BiddySelectNP(f);
3038 
3039  /* DEBUGGING */
3040  /*
3041  printf("NODE STARTED\n");
3042  BiddyDebugEdge(MNG,f);
3043  */
3044 
3045  n = 1;
3046  n += nodePlainNumber(MNG,
3047  Biddy_Managed_TransferMark(MNG,BiddyE(f),Biddy_GetMark(f),TRUE));
3048  n += nodePlainNumber(MNG,
3049  Biddy_Managed_TransferMark(MNG,BiddyT(f),Biddy_GetMark(f),FALSE));
3050 
3051  /* DEBUGGING */
3052  /*
3053  printf("NODE FINISHED\n");
3054  BiddyDebugEdge(MNG,f);
3055  printf("nodePlainNumber: return %u\n",n);
3056  */
3057 
3058  return n;
3059 }
3060 
3061 /*******************************************************************************
3062 \brief Function calculateSD.
3063 
3064 ### Description
3065 ### Side effects
3066 ### More info
3067 *******************************************************************************/
3068 
3069 static float
3070 calculateSD(unsigned long long int *data, unsigned int n)
3071 {
3072  float standardDeviation = 0.0;
3073 
3074 #ifdef BIDDYEXTENDEDSTATS_YES
3075  unsigned int i;
3076  unsigned long long int sum;
3077  float mean;
3078 
3079  sum = 0;
3080  for (i = 0; i < n; i++) {
3081  sum += data[i];
3082  }
3083 
3084  mean = (float) sum / (float) n;
3085 
3086  standardDeviation = 0;
3087  for (i=0; i<n; ++i) {
3088  standardDeviation += ((float) (data[i] - mean)) * ((float) (data[i] - mean));
3089  }
3090  standardDeviation = sqrt(standardDeviation/n);
3091 
3092  /*
3093  printf("(data: ");
3094  for (i=0; i<n; ++i) {
3095  printf("%llu",data[i]);
3096  if (i < n-1 ) printf(" "); else printf("), ");
3097  }
3098  printf("%.0f, %.0f, ",mean,standardDeviation);
3099  */
3100 #endif
3101 
3102  return standardDeviation;
3103 }
unsigned int Biddy_MaxLevel(Biddy_Edge f)
Function Biddy_MaxLevel.
Definition: biddyStat.c:164
Biddy_Variable is used for indices in variable table.
unsigned long long int Biddy_Managed_OPCacheFind(Biddy_Manager MNG)
Function Biddy_Managed_OPCacheFind.
Definition: biddyStat.c:1102
EXTERN void Biddy_Managed_SelectNode(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_SelectNode selects the top node of the given function.
Definition: biddyMain.c:1379
unsigned int Biddy_Managed_NodeTableGenerated(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGenerated.
Definition: biddyStat.c:308
EXTERN void Biddy_Managed_DeselectAll(Biddy_Manager MNG)
Function Biddy_Managed_DeselectAll deselects all nodes.
Definition: biddyMain.c:1515
unsigned long long int Biddy_Managed_NodeTableAddNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableAddNumber.
Definition: biddyStat.c:534
Biddy_Variable Biddy_Managed_VariableTableNum(Biddy_Manager MNG)
Function Biddy_Managed_VariableTableNum returns number of used variables.
Definition: biddyStat.c:228
unsigned int Biddy_Managed_NodeTableITENumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableITENumber.
Definition: biddyStat.c:734
float Biddy_AvgLevel(Biddy_Edge f)
Function Biddy_AvgLevel.
Definition: biddyStat.c:196
Biddy_Edge is a marked edge (i.e. a marked pointer to BiddyNode).
unsigned int Biddy_Managed_NodeTableSiftingNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableSiftingNumber.
Definition: biddyStat.c:684
float Biddy_Managed_ListAvgLength(Biddy_Manager MNG)
Function Biddy_Managed_ListAvgLength.
Definition: biddyStat.c:1035
EXTERN Biddy_String Biddy_Managed_GetVariableName(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableName returns the name of a variable.
Definition: biddyMain.c:1951
#define Biddy_GetMark(f)
Definition: biddy.h:168
unsigned int Biddy_Managed_ListMaxLength(Biddy_Manager MNG)
Function Biddy_Managed_ListMaxLength.
Definition: biddyStat.c:971
unsigned long long int Biddy_Managed_CountPaths(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountPaths count the number of 1-paths.
Definition: biddyStat.c:1457
unsigned int Biddy_Managed_DependentVariableNumber(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean select)
Function Biddy_Managed_DependentVariableNumber.
Definition: biddyStat.c:1279
unsigned long long int Biddy_Managed_OPCacheOverwrite(Biddy_Manager MNG)
Function Biddy_Managed_OPCacheOverwrite.
Definition: biddyStat.c:1158
unsigned int Biddy_Managed_NodeTableGCNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGCNumber.
Definition: biddyStat.c:565
unsigned int Biddy_Managed_NodeTableNum(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableNum returns number of all nodes currently in node table...
Definition: biddyStat.c:360
EXTERN Biddy_Edge Biddy_Managed_TransferMark(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean mark, Biddy_Boolean leftright)
Function Biddy_Managed_TransferMark returns edge with inverted complement bit iff the second paramete...
Definition: biddyMain.c:3096
unsigned int Biddy_Managed_MinNodes(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_MinNodes reports number of nodes in the optimal ordering.
Definition: biddyStat.c:1839
unsigned int Biddy_Managed_NodeTableGCTime(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGCTime.
Definition: biddyStat.c:590
EXTERN Biddy_Boolean Biddy_Managed_FindFormula(Biddy_Manager MNG, Biddy_String x, unsigned int *idx, Biddy_Edge *f)
Function Biddy_Managed_FindFormula find formula in Formula table.
Definition: biddyMain.c:4759
unsigned int Biddy_Managed_NodeTableSize(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableSize returns the size of node table.
Definition: biddyStat.c:253
EXTERN Biddy_Variable Biddy_Managed_GetLowestVariable(Biddy_Manager MNG)
Function Biddy_Managed_GetLowestVariable returns the lowest variable in the current ordering...
Definition: biddyMain.c:1766
unsigned long long int Biddy_Managed_NodeTableGCObsoleteNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGCObsoleteNumber.
Definition: biddyStat.c:619
Biddy_String is used for strings.
unsigned int Biddy_Managed_FormulaTableNum(Biddy_Manager MNG)
Function Biddy_Managed_FormulaTableNum returns number of known formulae.
Definition: biddyStat.c:913
EXTERN int Biddy_Managed_GetManagerType(Biddy_Manager MNG)
Function Biddy_Managed_GetManagerType reports BDD type used in the manager.
Definition: biddyMain.c:1129
double Biddy_Managed_DensityOfFunction(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
Function Biddy_Managed_DensityOfFunction calculates the ratio of the number of on-set minterms to the...
Definition: biddyStat.c:1670
unsigned long long int Biddy_Managed_NodeTableXORRecursiveNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableXORRecursiveNumber.
Definition: biddyStat.c:881
unsigned int Biddy_Managed_ListUsed(Biddy_Manager MNG)
Function Biddy_Managed_ListUsed.
Definition: biddyStat.c:938
unsigned int Biddy_Managed_CountComplementedEdges(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountComplementedEdges count the number of complemented edges.
Definition: biddyStat.c:1401
unsigned long long int Biddy_Managed_NodeTableCompareNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableCompareNumber.
Definition: biddyStat.c:502
EXTERN Biddy_Variable Biddy_Managed_AddVariableByName(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_AddVariableByName adds variable.
Definition: biddyMain.c:2871
unsigned int Biddy_Managed_CountNodes(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountNodes.
Definition: biddyStat.c:85
double Biddy_Managed_CountMinterms(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
Function Biddy_Managed_CountMinterms.
Definition: biddyStat.c:1526
Biddy_Boolean is used for boolean values.
unsigned int Biddy_Managed_MaxNodes(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_MaxNodes reports number of nodes in the worst ordering.
Definition: biddyStat.c:1982
unsigned long long int Biddy_Managed_NodeTableITERecursiveNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableITERecursiveNumber.
Definition: biddyStat.c:762
#define Biddy_GetTag(f)
Definition: biddy.h:199
unsigned int Biddy_Managed_NodeTableNumVar(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_NodeTableNumVar returns number of nodes with a given variable currently in nod...
Definition: biddyStat.c:386
#define Biddy_IsNull(f)
Definition: biddy.h:150
unsigned long long int Biddy_Managed_NodeTableFindNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableFindNumber.
Definition: biddyStat.c:470
unsigned long long int Biddy_Managed_OPCacheInsert(Biddy_Manager MNG)
Function Biddy_Managed_OPCacheInsert.
Definition: biddyStat.c:1127
double Biddy_Managed_DensityOfBDD(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
Function Biddy_Managed_DensityOfBDD calculates the ratio of the number of on-set minterms to the numb...
Definition: biddyStat.c:1743
EXTERN Biddy_String Biddy_Managed_GetManagerName(Biddy_Manager MNG)
Function Biddy_Managed_GetManagerName reports the name of the BDD type used in the manager...
Definition: biddyMain.c:1155
EXTERN void Biddy_ExitMNG(Biddy_Manager *mng)
Function Biddy_ExitMNG deletes a manager.
Definition: biddyMain.c:883
unsigned long long int Biddy_Managed_ReadMemoryInUse(Biddy_Manager MNG)
Function Biddy_Managed_ReadMemoryInUse reports memory consumption of main data strucutures in bytes (...
Definition: biddyStat.c:2124
unsigned long long int Biddy_Managed_OPCacheSearch(Biddy_Manager MNG)
Function Biddy_Managed_OPCacheSearch.
Definition: biddyStat.c:1077
Biddy_Manager is used to specify manager.
unsigned int Biddy_Managed_NodeTableSwapNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableSwapNumber.
Definition: biddyStat.c:658
unsigned int Biddy_Managed_NodeTableMax(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableMax returns maximal (peek) number of nodes in node table...
Definition: biddyStat.c:334
#define Biddy_IsTerminal(f)
Definition: biddy.h:160
unsigned int Biddy_Managed_NodeTableXORNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableXORNumber.
Definition: biddyStat.c:853
void Biddy_Managed_PrintInfo(Biddy_Manager MNG, FILE *f)
Function Biddy_Managed_PrintInfo prepares a file with stats.
Definition: biddyStat.c:2221
unsigned int Biddy_Managed_NodeTableDRTime(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableDRTime.
Definition: biddyStat.c:709
unsigned int Biddy_Managed_NodeTableBlockNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableBlockNumber.
Definition: biddyStat.c:283
File biddyInt.h contains declaration of internal data structures.
unsigned int Biddy_Managed_NodeTableResizeNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableResizeNumber.
Definition: biddyStat.c:412
EXTERN Biddy_Boolean Biddy_Managed_IsSelected(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_IsSelected returns TRUE iff the top node of the given function is selected...
Definition: biddyMain.c:1431
unsigned long long int Biddy_Managed_NodeTableFoaNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableFoaNumber.
Definition: biddyStat.c:438
EXTERN void Biddy_InitMNG(Biddy_Manager *mng, int bddtype)
Function Biddy_InitMNG initialize a manager.
Definition: biddyMain.c:177
unsigned int Biddy_Managed_CountNodesPlain(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountNodesPlain.
Definition: biddyStat.c:1191
unsigned long long int Biddy_Managed_NodeTableANDORRecursiveNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableANDORRecursiveNumber.
Definition: biddyStat.c:822
unsigned int Biddy_Managed_NodeTableANDORNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableANDORNumber.
Definition: biddyStat.c:794