Biddy  1.7.3
An academic Binary Decision Diagrams package
biddy-example-independence.c
1 /* $Revision: 300 $ */
2 /* $Date: 2017-09-08 15:51:12 +0200 (pet, 08 sep 2017) $ */
3 /* This file (biddy-example-independence.c) is a C file */
4 /* Author: Robert Meolic (robert.meolic@um.si) */
5 /* This file has been released into the public domain by the author. */
6 
7 /* This example is compatible with Biddy v1.7 and CUDD v3.0.0 */
8 
9 /* COMPILE WITH: */
10 /* gcc -DNOCONVERGE -DNOPROFILE -DUNIX -DUSE_BIDDY -O2 -o biddy-example-independence biddy-example-independence.c biddy-example-independence-usa.c biddy-example-independence-europe.c -I. -L./bin -lbiddy -lgmp */
11 /* gcc -DNOCONVERGE -DNOPROFILE -DUSE_CUDD -O2 -o cudd-example-independence biddy-example-independence.c biddy-example-independence-usa.c biddy-example-independence-europe.c -I ../cudd/include/ -L ../cudd/lib/ -lcudd -lm */
12 
13 /* define CALCULATE_KERNELS 0 OR 1 */
14 /* define USA_NO or USA_YES */
15 /* define EUROPE_NO or EUROPE_YES */
16 #define CALCULATE_KERNELS 0
17 #define USA_YES
18 #define EUROPE_YES
19 
20 #ifdef USE_BIDDY
21 # include "biddy.h"
22 # include <string.h>
23 # define BDDNULL NULL
24 #endif
25 
26 #ifdef USE_CUDD
27 # include <stdio.h>
28 # include <stdlib.h>
29 # include <stdint.h>
30 # include <stdarg.h>
31 # include <ctype.h>
32 # include <string.h>
33 # include <math.h>
34 # include "cudd.h"
35 # define BDDNULL NULL
36 # ifndef TRUE
37 # define TRUE (0 == 0)
38 # endif
39 # ifndef FALSE
40 # define FALSE !TRUE
41 # endif
42 typedef char *Biddy_String;
43 typedef char Biddy_Boolean;
44 typedef DdNode *Biddy_Edge;
45 DdManager *manager;
46 #endif
47 
48 #include <time.h>
49 
50 #ifdef USE_CUDD
51 #define BIDDYTYPEOBDD 1
52 #define BIDDYTYPEOBDDC 2
53 #define BIDDYTYPEZBDD 3
54 #define BIDDYTYPEZBDDC 4
55 #define BIDDYTYPETZBDD 5
56 #define BIDDYTYPETZBDDC 6
57 #define Biddy_GetManagerType() BIDDYTYPEOBDDC
58 #define Biddy_GetConstantZero() Cudd_ReadLogicZero(manager)
59 #define Biddy_GetConstantOne() Cudd_ReadOne(manager)
60 #define Biddy_AddVariable() Cudd_bddNewVar(manager)
61 #define Biddy_Not(f) Cudd_Not(f)
62 #define Biddy_And(f,g) Cudd_bddAnd(manager,f,g)
63 #define Biddy_Or(f,g) Cudd_bddOr(manager,f,g)
64 #define Biddy_Xor(f,g) Cudd_bddXor(manager,f,g)
65 #define Biddy_Xnor(f,g) Cudd_bddXnor(manager,f,g)
66 #define Biddy_Support(f) Cudd_Support(manager,f)
67 #define Biddy_DependentVariableNumber(f) Cudd_SupportSize(manager,f)
68 #define Biddy_CountMinterm(f,n) Cudd_CountMinterm(manager,f,n)
69 #define Biddy_NodeNumber(f) Cudd_DagSize(f)
70 #define Biddy_NodeTableNum() Cudd_ReadKeys(manager)
71 #define Biddy_NodeTableSize() Cudd_ReadSlots(manager)
72 #define Biddy_PrintInfo(s) Cudd_PrintInfo(manager,s)
73 #endif
74 
75 extern void setDataUSA(unsigned int *size, unsigned int ***usa, unsigned int **order, char **codes);
76 extern void setDataEurope(unsigned int *size, unsigned int ***europe, unsigned int **order, char **codes);
77 static void createGraph(unsigned int size, unsigned int **edge, Biddy_Edge *state, Biddy_Edge *graph);
78 static Biddy_Edge calculateIndependence(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph);
79 static Biddy_Edge calculateKernels(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph);
80 static void writeOrder(Biddy_Edge f, char *codes, unsigned int *order, unsigned int size);
81 
82 int main(int argc, char** argv) {
83  unsigned int i;
84  Biddy_Boolean complete;
85  Biddy_Edge tmp;
86  Biddy_Edge r1,r2;
87  unsigned int n1,n2;
88  char *userinput;
89 
90  clock_t elapsedtime;
91 
92 #ifdef USA_YES
93  unsigned int usaSize = 0;
94  unsigned int **usaEdge;
95  unsigned int *usaOrder;
96  char *usaCodes;
97  Biddy_Edge *usaState;
98  Biddy_Edge *usaGraph;
99 #endif
100 
101 #ifdef EUROPE_YES
102  unsigned int europeSize = 0;
103  unsigned int **europeEdge;
104  unsigned int *europeOrder;
105  char *europeCodes;
106  Biddy_Edge *europeState;
107  Biddy_Edge *europeGraph;
108 #endif
109 
110  setbuf(stdout, NULL);
111 
112 #ifdef USA_YES
113  setDataUSA(&usaSize,&usaEdge,&usaOrder,&usaCodes);
114 #endif
115 
116 #ifdef EUROPE_YES
117  setDataEurope(&europeSize,&europeEdge,&europeOrder,&europeCodes);
118 #endif
119 
120 #ifdef USE_BIDDY
121  /* There is only one unique table in Biddy */
122  /* There are several caches in Biddy */
123  /* Unique table grows over the time */
124  /* The max number of variables is hardcoded in biddyInt. h */
125  /* biddyVariableTable.size = BIDDYVARMAX = 2048 */
126  /* The following constants are hardcoded in biddyMain.c */
127  /* biddyIteCache.size = MEDIUM_TABLE = 262143 */
128  /* biddyEACache.size = SMALL_TABLE = 65535 */
129  /* biddyRCCache.size = SMALL_TABLE = 65535 */
130  /* DEFAULT INIT CALL: Biddy_InitAnonymous(BIDDYTYPEOBDDC) */
131  Biddy_InitAnonymous(BIDDYTYPEOBDDC);
132  if (argc == 1) {
133  Biddy_SetManagerParameters(-1,-1,-1,-1,-1,-1,-1,-1,-1,-1);
134  }
135  else if (argc == 7) {
136  int gcr,gcrF,gcrX;
137  int rr,rrF,rrX;
138  sscanf(argv[1],"%d",&gcr);
139  sscanf(argv[2],"%d",&gcrF);
140  sscanf(argv[3],"%d",&gcrX);
141  sscanf(argv[4],"%d",&rr);
142  sscanf(argv[5],"%d",&rrF);
143  sscanf(argv[6],"%d",&rrX);
144  Biddy_SetManagerParameters(gcr/100.0,gcrF/100.0,gcrX/100.0,rr/100.0,rrF/100.0,rrX/100.0,-1,-1,-1,-1);
145  printf("%d, %d, %d, %d, %d, %d, ",gcr,gcrF,gcrX,rr,rrF,rrX);
146  }
147  else if (argc == 11) {
148  int gcr,gcrF,gcrX;
149  int rr,rrF,rrX;
150  int st;
151  int fst;
152  int cst;
153  int fcst;
154  sscanf(argv[1],"%d",&gcr);
155  sscanf(argv[2],"%d",&gcrF);
156  sscanf(argv[3],"%d",&gcrX);
157  sscanf(argv[4],"%d",&rr);
158  sscanf(argv[5],"%d",&rrF);
159  sscanf(argv[6],"%d",&rrX);
160  sscanf(argv[7],"%d",&st);
161  sscanf(argv[8],"%d",&fst);
162  sscanf(argv[9],"%d",&cst);
163  sscanf(argv[10],"%d",&fcst);
164  Biddy_SetManagerParameters(gcr/100.0,gcrF/100.0,gcrX/100.0,rr/100.0,rrF/100.0,rrX/100.0,st/100.0,fst/100.0,cst/100.0,fcst/100.0);
165  printf("%d, %d, %d, %d, %d, %d, ",gcr,gcrF,gcrX,rr,rrF,rrX);
166  }
167  else {
168  printf("Wrong number of parameters!\n");
169  exit(0);
170  }
171 #endif
172 
173 #ifdef USE_CUDD
174  /* In CUDD each variable has its own subtable in the unique table */
175  /* There is only one cache in CUDD */
176  /* Subtables grow over the time, you can set limit for fast unique table growth */
177  /* Cudd_SetLooseUpTo(manager,1048576) */
178  /* Cache can grow over the time, you can set the max size */
179  /* Cudd_SetMaxCacheHard(manager,262144) */
180  /* These two constants are hardcoded in v3.0.0 */
181  /* CUDD_UNIQUE_SLOTS = 256 (default initial size of each subtable) */
182  /* CUDD_CACHE_SLOTS = 262144 (default initial size of cache table) */
183  /* DEFAULT INIT CALL: Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0) */
184  manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
185  Cudd_SetMaxCacheHard(manager,262144);
186 #endif
187 
188 #ifdef USA_YES
189  usaGraph = (Biddy_Edge *) malloc(usaSize*sizeof(Biddy_Edge *));
190  usaState = (Biddy_Edge *) malloc(usaSize*sizeof(Biddy_Edge *));
191 #endif
192 
193 #ifdef EUROPE_YES
194  europeGraph = (Biddy_Edge *) malloc(europeSize*sizeof(Biddy_Edge *));
195  europeState = (Biddy_Edge *) malloc(europeSize*sizeof(Biddy_Edge *));
196 #endif
197 
198  /* create BDD variables */
199  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC) ||
200  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDD))
201  {
202 
203  i = 0;
204  complete = FALSE;
205  while (!complete) {
206  complete = TRUE;
207  tmp = Biddy_AddVariable();
208 #ifdef USA_YES
209  if (i < usaSize) {
210  usaState[usaOrder[i]] = tmp;
211  }
212  complete = complete && (i >= (usaSize-1));
213 #endif
214 #ifdef EUROPE_YES
215  if (i < europeSize) {
216  europeState[europeOrder[i]] = tmp;
217  }
218  complete = complete && (i >= (europeSize-1));
219 #endif
220  i++;
221  }
222 #ifdef USE_BIDDY
223  Biddy_Purge(); /* remove unnecessary nodes, this is useful only for ZBDDs */
224 #endif
225 
226  }
227 
228  /* for ZBDDs, by adding new variables all the existing ones are changed */
229  /* after adding the last variable we have to refresh them all */
230  /* NOTE: for Biddy, ZBDD variables are added in the reverse order to get consistent results */
231  /* NOTE: for CUDD, usaState[0] = europeState[0] and it is first added */
232  /* NOTE: for Biddy, usaState[0] = europeState[0] and it is last added */
233  /* NOTE: for Biddy, user variables start with index 1 */
234  /* NOTE: for CUDD, user variables start with index 0 */
235  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC))
236  {
237 
238  i = 0;
239  complete = FALSE;
240  while (!complete) {
241  complete = TRUE;
242  tmp = Biddy_AddVariable();
243 #ifdef USA_YES
244  if (i < usaSize) {
245 #ifdef USE_CUDD
246  usaState[usaOrder[i]] = tmp;
247 #endif
248 #ifdef USE_BIDDY
249  usaState[usaSize-usaOrder[i]-1] = tmp;
250 #endif
251  }
252  complete = complete && (i >= (usaSize-1));
253 #endif
254 #ifdef EUROPE_YES
255  if (i < europeSize) {
256 #ifdef USE_CUDD
257  europeState[europeOrder[i]] = tmp;
258 #endif
259 #ifdef USE_BIDDY
260  europeState[europeSize-europeOrder[i]-1] = tmp;
261 #endif
262  }
263  complete = complete && (i >= (europeSize-1));
264 #endif
265  i++;
266  }
267 #ifdef USE_BIDDY
268  i = 0;
269  complete = FALSE;
270  while (!complete) {
271  complete = TRUE;
272 #ifdef USA_YES
273  if (i < usaSize) {
274  usaState[usaOrder[i]] = Biddy_GetVariableEdge(usaSize-i);
275  }
276  complete = complete && (i >= (usaSize-1));
277 #endif
278 #ifdef EUROPE_YES
279  if (i < europeSize) {
280  europeState[europeOrder[i]] = Biddy_GetVariableEdge(europeSize-i);
281  }
282  complete = complete && (i >= (europeSize-1));
283 #endif
284  i++;
285  }
286  Biddy_Purge(); /* remove unnecessary nodes, this is useful only for ZBDDs */
287 #endif
288 #ifdef USE_CUDD
289  i = 0;
290  complete = FALSE;
291  while (!complete) {
292  complete = TRUE;
293 #ifdef USA_YES
294  if (i < usaSize) {
295  Cudd_RecursiveDeref(manager,usaState[usaOrder[i]]);
296  usaState[usaOrder[i]] = Cudd_zddIthVar(manager,i);
297  Cudd_Ref(usaState[usaOrder[i]]);
298  }
299  complete = complete && (i >= (usaSize-1));
300 #endif
301 #ifdef EUROPE_YES
302  if (i < europeSize) {
303  Cudd_RecursiveDeref(manager,europeState[europeOrder[i]]);
304  europeState[europeOrder[i]] = Cudd_zddIthVar(manager,i);
305  Cudd_Ref(europeState[europeOrder[i]]);
306  }
307  complete = complete && (i >= (europeSize-1));
308 #endif
309  i++;
310  }
311 #endif
312 
313  }
314 
315  /* HERE, BDD OPERATIONS START AND THUS WE START TO MEASURE THE TIME */
316  elapsedtime = clock();
317 
318 #ifdef USA_YES
319  createGraph(usaSize,usaEdge,usaState,usaGraph);
320 #endif
321 
322 #ifdef EUROPE_YES
323  createGraph(europeSize,europeEdge,europeState,europeGraph);
324 #endif
325 
326  r1 = Biddy_GetConstantZero();
327  r2 = Biddy_GetConstantZero();
328 #ifdef USE_CUDD
329  Cudd_Ref(r1);
330  Cudd_Ref(r2);
331 #endif
332 
333 #ifdef USA_YES
334  if (!CALCULATE_KERNELS) {
335  /* CALCULATING INDEPENDENCE SETS FOR USA */
336 #ifdef USE_CUDD
337  Cudd_RecursiveDeref(manager,r1);
338 #endif
339  r1 = calculateIndependence(usaSize,usaState,usaGraph);
340  } else {
341  /* CALCULATING KERNELS (MAXIMUM INDEPENDENCE SETS) FOR USA */
342 #ifdef USE_CUDD
343  Cudd_RecursiveDeref(manager,r1);
344 #endif
345  r1 = calculateKernels(usaSize,usaState,usaGraph);
346  }
347 #ifdef USE_BIDDY
348  Biddy_AddPersistentFormula((Biddy_String)"usa",r1);
349 #endif
350 #ifdef USE_CUDD
351  for (i=0; i<usaSize; i++) {
352  Cudd_RecursiveDeref(manager,usaGraph[i]);
353  }
354 #endif
355 #endif
356 
357 #ifdef EUROPE_YES
358  if (!CALCULATE_KERNELS) {
359  /* CALCULATING INDEPENDENCE SETS FOR EUROPE */
360 #ifdef USE_CUDD
361  Cudd_RecursiveDeref(manager,r2);
362 #endif
363  r2 = calculateIndependence(europeSize,europeState,europeGraph);
364  } else {
365  /* CALCULATING KERNELS (MAXIMUM INDEPENDENCE SETS) FOR EUROPE */
366 #ifdef USE_CUDD
367  Cudd_RecursiveDeref(manager,r2);
368 #endif
369  r2 = calculateKernels(europeSize,europeState,europeGraph);
370  }
371 #ifdef USE_BIDDY
372  Biddy_AddPersistentFormula((Biddy_String)"europe",r2);
373 #endif
374 #ifdef USE_CUDD
375  for (i=0; i<europeSize; i++) {
376  Cudd_RecursiveDeref(manager,europeGraph[i]);
377  }
378 #endif
379 #endif
380 
381 #ifdef USE_BIDDY
382  /* TO GET RELEVANT TIME FOR SIFTING WE HAVE TO REMOVE UNNECESSARY NODES */
383  /* this will remove all tmp formulae created by createGraph() */
384  Biddy_Purge();
385 #endif
386 
387  userinput = strdup("...");
388  while (userinput[0] != 'x') {
389 
390  /* We have problems with passing stdout in the case you compile this file */
391  /* with MINGW and use biddy.dll generated with Visual Studio. */
392  /* In such cases, please, use Biddy_PrintInfo(NULL) */
393  if (userinput[0] == 'r') Biddy_PrintInfo(stdout);
394 
395  /* SIFTING */
396 #ifdef USE_BIDDY
397 #ifdef CONVERGE
398  if (userinput[0] == 's') Biddy_Sifting(NULL,TRUE);
399 #ifdef USA_YES
400  if (userinput[0] == 'u') Biddy_Sifting(r1,TRUE);
401 #endif
402 #ifdef EUROPE_YES
403  if (userinput[0] == 'e') Biddy_Sifting(r2,TRUE);
404 #endif
405 #else
406  if (userinput[0] == 's') Biddy_Sifting(NULL,FALSE);
407 #ifdef USA_YES
408  if (userinput[0] == 'u') Biddy_Sifting(r1,FALSE);
409 #endif
410 #ifdef EUROPE_YES
411  if (userinput[0] == 'e') Biddy_Sifting(r2,FALSE);
412 #endif
413 #endif
414  /* for TZBDD, sifting may change top node! */
415 #ifdef USA_YES
416  if (!Biddy_FindFormula((Biddy_String)"usa",&i,&r1)) exit(99);
417 #endif
418 #ifdef EUROPE_YES
419  if (!Biddy_FindFormula((Biddy_String)"europe",&i,&r2)) exit(99);
420 #endif
421 #endif
422 #ifdef USE_CUDD
423 #ifdef CONVERGE
424  if (userinput[0] == 's') Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT_CONVERGE,0);
425 #else
426  if (userinput[0] == 's') Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT,0);
427 #endif
428 #endif
429 
432 
433  if ((userinput[0] == 's')
434 #ifdef USA_YES
435  || (userinput[0] == 'u')
436 #endif
437 #ifdef EUROPE_YES
438  || (userinput[0] == 'e')
439 #endif
440  ) {
441 #ifdef CONVERGE
442  printf("(CONVERGING SIFTING");
443 #ifdef USE_BIDDY
444  if (userinput[0] == 'u') {
445  printf(" ON FUNCTION FOR USA");
446  }
447  if (userinput[0] == 'e') {
448  printf(" ON FUNCTION FOR EUROPE");
449  }
450 #endif
451 #ifdef PROFILE
452  printf("), ");
453 #else
454  printf(")\n");
455 #endif
456 #else
457  printf("(SIFTING");
458 #ifdef USE_BIDDY
459  if (userinput[0] == 'u') {
460  printf(" ON FUNCTION FOR USA");
461  }
462  if (userinput[0] == 'e') {
463  printf(" ON FUNCTION FOR EUROPE");
464  }
465 #endif
466 #ifdef PROFILE
467  printf("), ");
468 #else
469  printf(")\n");
470 #endif
471 #endif
472  }
473 
474 #ifndef PROFILE
475  printf("Resulting function r1/r2 depends on %u/%u variables.\n",n1,n2);
476  printf("Resulting function r1/r2 has %.0f/%.0f minterms.\n",Biddy_CountMinterm(r1,n1),Biddy_CountMinterm(r2,n2));
477  printf("BDD system has %u nodes.\n",Biddy_NodeTableNum());
478 #ifdef USE_BIDDY
479  if (Biddy_GetManagerType() == BIDDYTYPEOBDDC) {
480  printf("OBDDC");
481  } else if (Biddy_GetManagerType() == BIDDYTYPEZBDDC) {
482  printf("ZBDDC");
483  } else if (Biddy_GetManagerType() == BIDDYTYPETZBDD) {
484  printf("TZBDD");
485  }
486  printf(" for resulting function r1/r2 has %u/%u nodes (%u/%u nodes if using complement edges).\n",
488 #endif
489 #ifdef USE_CUDD
490  printf("BDD for resulting function r1/r2 has %u/%u nodes (using complement edges).\n",Biddy_NodeNumber(r1),Biddy_NodeNumber(r2));
491 #endif
492 #ifdef USE_BIDDY
493  printf("Variable swaps performed so far: %u\n",Biddy_NodeTableSwapNumber());
494 #endif
495 #ifdef USE_CUDD
496  printf("Variable swaps performed so far: %.0f\n",Cudd_ReadSwapSteps(manager));
497 #endif
498 #endif
499 #ifndef PROFILE
500 #ifdef USA_YES
501  printf("Order for USA: ");
502  writeOrder(r1,usaCodes,usaOrder,usaSize);
503 #endif
504 #ifdef EUROPE_YES
505  printf("Order for Europe: ");
506  writeOrder(r2,europeCodes,europeOrder,europeSize);
507 #endif
508 #endif
509 #ifndef PROFILE
510 #ifdef USE_BIDDY
511  printf("E[x]it or [r]eport or ");
512 #ifdef CONVERGE
513  printf("Converging sifting ");
514 #else
515  printf("Sifting ");
516 #endif
517 #if (defined USA_YES) || (defined EUROPE_YES)
518  printf("on [s]ystem or on function for");
519 #ifdef USA_YES
520  printf(" [u]SA");
521 #endif
522 #ifdef EUROPE_YES
523  printf(" [e]urope");
524 #endif
525 #endif
526 #endif
527 #ifdef USE_CUDD
528  printf("E[x]it or [r]eport or ");
529 #ifdef CONVERGE
530  printf("Converging sifting ");
531 #else
532  printf("Sifting ");
533 #endif
534  printf("on [s]ystem");
535 #endif
536  printf(": ");
537 #endif
538 #ifdef PROFILE
539  if (!strcmp(userinput,"r")) userinput = strdup("x");
540  if (!strcmp(userinput,"s")) userinput = strdup("x");
541  if (!strcmp(userinput,"...")) userinput = strdup("s");
542 #else
543  if (!scanf("%s",userinput)) printf("ERROR\n");
544 #endif
545  }
546 
547  elapsedtime = clock()-elapsedtime;
548 
549  free(userinput);
550 
551  /* PROFILING */
552  /**/
553 #ifdef USE_BIDDY
554 #ifdef MINGW
555  fprintf(stderr,"%I64u, %.2f",Biddy_ReadMemoryInUse(),Biddy_NodeTableDRTime())/(1.0*CLOCKS_PER_SEC);
556 #else
557  fprintf(stderr,"%llu, %.2f",Biddy_ReadMemoryInUse(),Biddy_NodeTableDRTime()/(1.0*CLOCKS_PER_SEC));
558 #endif
559  printf(", %u/%u",Biddy_NodeNumber(r1),Biddy_NodeNumber(r2));
560  fprintf(stderr,"\n");
561 #endif
562 
563  /* EXIT */
564 #ifdef USE_BIDDY
565  Biddy_Exit();
566 #endif
567 #ifdef USE_CUDD
568  Cudd_RecursiveDeref(manager,r1);
569  Cudd_RecursiveDeref(manager,r2);
570  printf("CUDD: nodes with non-zero reference counts: %d\n",Cudd_CheckZeroRef(manager));
571  Cudd_Quit(manager);
572 #endif
573 
574  return 0;
575 }
576 
577 /* CREATE GRAPH */
578 static void createGraph(unsigned int size, unsigned int **edge, Biddy_Edge *state, Biddy_Edge *graph) {
579  unsigned int i,j;
580  Biddy_Edge tmp;
581  /*
582  printf("CREATE GRAPH... ");
583  */
584  for (i=0; i<size; i++) {
585  graph[i] = Biddy_GetConstantZero();
586 #ifdef USE_CUDD
587  Cudd_Ref(graph[i]);
588 #endif
589  for (j=0; j<size; j++) {
590  if (edge[i][j]) {
591  tmp = Biddy_Or(graph[i],state[j]);
592 #ifdef USE_CUDD
593  Cudd_Ref(tmp);
594  Cudd_RecursiveDeref(manager,graph[i]);
595 #endif
596  graph[i] = tmp;
597  }
598  }
599 #ifdef USE_BIDDY
600  Biddy_AddTmpFormula(graph[i],0);
601 #endif
602  }
603  /*
604  printf("OK\n");
605  */
606 }
607 
608 /* CALCULATE INDEPENDENCE SETS */
609 static Biddy_Edge calculateIndependence(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph) {
610  unsigned int i;
611  Biddy_Edge p,r,tmp;
612  /*
613  printf("CALCULATE INDEPENDENCE SETS...\n");
614  */
615  r = Biddy_GetConstantZero();
616 #ifdef USE_CUDD
617  Cudd_Ref(r);
618 #endif
619  for (i=0; i<size; i++) {
620  p = Biddy_And(graph[i],state[i]);
621 #ifdef USE_CUDD
622  Cudd_Ref(p);
623 #endif
624  tmp = Biddy_Or(r,p);
625 #ifdef USE_BIDDY
626  Biddy_AddTmpFormula(tmp,1);
627  Biddy_Clean();
628 #endif
629 #ifdef USE_CUDD
630  Cudd_Ref(tmp);
631  Cudd_RecursiveDeref(manager,r);
632  Cudd_RecursiveDeref(manager,p);
633  /* Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT,0); */
634 #endif
635  r = tmp;
636  }
637  return Biddy_Not(r);
638 }
639 
640 /* CALCULATE KERNELS (MAXIMUM INDEPENDENCE SETS) */
641 static Biddy_Edge calculateKernels(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph) {
642  unsigned int i;
643  Biddy_Edge p,r,tmp;
644  /*
645  printf("CALCULATE KERNELS (MAXIMUM INDEPENDENCE SETS)...\n");
646  */
647  r = Biddy_GetConstantZero();
648 #ifdef USE_CUDD
649  Cudd_Ref(r);
650 #endif
651  for (i=0; i<size; i++) {
652  p = Biddy_Xnor(graph[i],state[i]);
653 #ifdef USE_CUDD
654  Cudd_Ref(p);
655 #endif
656  tmp = Biddy_Or(r,p);
657 #ifdef USE_BIDDY
658  Biddy_AddTmpFormula(tmp,1);
659  Biddy_Clean();
660 #endif
661 #ifdef USE_CUDD
662  Cudd_Ref(tmp);
663  Cudd_RecursiveDeref(manager,r);
664  Cudd_RecursiveDeref(manager,p);
665  /* Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT,0); */
666 #endif
667  r = tmp;
668  }
669  return Biddy_Not(r);
670 }
671 
672 static void writeOrder(Biddy_Edge f, char *codes, unsigned int *order, unsigned int size) {
673  char ch;
674 #ifdef USE_CUDD
675  int i, j;
676 #endif
677  int k;
678  unsigned int ivar = 0;
679 
680 #ifdef USE_BIDDY
681  /* TO DO: IMPLEMENT Biddy_ReadPerm() AND ITS INVERSE */
682  {
683  Biddy_Edge tmp;
684  tmp = Biddy_Support(f);
685  while (!Biddy_IsConstant(tmp)) {
686  /* In Biddy, the first user variable is at index [1] */
687  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC)) {
688  ivar = Biddy_GetTopVariable(tmp)-1;
689  } else if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC)) {
690  ivar = size - Biddy_GetTopVariable(tmp);
691  } else if ((Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC)) {
692  ivar = Biddy_GetTopVariable(tmp)-1;
693  }
694  k = 3*(order[ivar]);
695  ch = codes[k+2];
696  codes[k+2] = 0;
697  printf("%s",&codes[k]);
698  codes[k+2] = ch;
699  tmp = Biddy_GetThen(tmp);
700  if (!Biddy_IsConstant(tmp)) printf(","); else printf("\n");
701  }
702  Biddy_Purge(); /* we do not want that removing tmp nodes is part of benchmarks */
703  }
704 #endif
705 
706 #ifdef USE_CUDD
707  /* HOW TO AVOID THIS DOUBLE LOOP ??? */
708  for (i=0; i<size; i++) {
709  /* In CUDD, the first user variable is at index [0] */
710  for (j=0; j<size; j++) {
711  if (i == Cudd_ReadPerm(manager,j)) ivar = j;
712  }
713  k = 3*(order[ivar]);
714  ch = codes[k+2];
715  codes[k+2] = 0;
716  printf("%s", &codes[k]);
717  codes[k+2] = ch;
718  if (i != (size-1)) printf(","); else printf("\n");
719  }
720 #endif
721 
722 }
#define Biddy_CountMinterm(f, nvars)
Definition: biddy.h:982
void * Biddy_Edge
Definition: biddy.h:250
#define Biddy_GetManagerType()
Definition: biddy.h:309
#define Biddy_And(f, g)
Definition: biddy.h:517
#define Biddy_Purge()
Definition: biddy.h:668
#define Biddy_Sifting(f, c)
Definition: biddy.h:735
#define Biddy_Clean()
Definition: biddy.h:663
#define Biddy_Xnor(f, g)
Definition: biddy.h:547
#define Biddy_NodeTableNum()
Definition: biddy.h:821
Biddy_Edge Biddy_GetThen(Biddy_Edge fun)
Function Biddy_GetThen returns THEN successor.
Definition: biddyMain.c:1018
Biddy_Variable Biddy_GetTopVariable(Biddy_Edge fun)
Function Biddy_GetTopVariable returns the top variable.
Definition: biddyMain.c:1090
#define Biddy_DependentVariableNumber(f)
Definition: biddy.h:961
#define Biddy_NodeNumberPlain(f)
Definition: biddy.h:956
#define Biddy_PrintInfo(f)
Definition: biddy.h:1004
#define Biddy_Or(f, g)
Definition: biddy.h:525
#define Biddy_FindFormula(x, idx, f)
Definition: biddy.h:700
#define Biddy_NodeNumber(f)
Definition: biddy.h:781
#define Biddy_NodeTableSwapNumber()
Definition: biddy.h:871
#define Biddy_Not(f)
Definition: biddy.h:506
#define Biddy_NodeTableDRTime()
Definition: biddy.h:881
#define Biddy_GetConstantZero()
Definition: biddy.h:374
#define Biddy_Exit()
Definition: biddy.h:301
File biddy.h contains declaration of all external data structures.
#define Biddy_Support(f)
Definition: biddy.h:621
char Biddy_Boolean
Definition: biddy.h:220
#define Biddy_GetVariableEdge(v)
Definition: biddy.h:408
#define Biddy_ReadMemoryInUse()
Definition: biddy.h:999
#define Biddy_SetManagerParameters(gcr, gcrF, gcrX, rr, rrF, rrX, st, fst, cst, fcst)
Definition: biddy.h:319
#define Biddy_IsConstant(f)
Definition: biddy.h:159
char * Biddy_String
Definition: biddy.h:223