Biddy  1.7.1
An academic Binary Decision Diagrams package
biddy-example-independence.c
1 /* $Revision: 253 $ */
2 /* $Date: 2017-03-20 09:03:47 +0100 (pon, 20 mar 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 -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 -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 /* #define Biddy_Inv(f) Biddy_NOT(f) */ /* for compatibility with Biddy v1.6 */
25 #endif
26 
27 #ifdef USE_CUDD
28 # include <stdio.h>
29 # include <stdlib.h>
30 # include <stdint.h>
31 # include <stdarg.h>
32 # include <ctype.h>
33 # include <string.h>
34 # include <math.h>
35 # include "cudd.h"
36 # define BDDNULL NULL
37 # ifndef TRUE
38 # define TRUE (0 == 0)
39 # endif
40 # ifndef FALSE
41 # define FALSE !TRUE
42 # endif
43 typedef char *Biddy_String;
44 typedef char Biddy_Boolean;
45 typedef DdNode *Biddy_Edge;
46 DdManager *manager;
47 #endif
48 
49 #ifdef USE_CUDD
50 #define Biddy_GetConstantZero() Cudd_ReadLogicZero(manager)
51 #define Biddy_GetConstantOne() Cudd_ReadOne(manager)
52 #define Biddy_GetElse(f) Cudd_E(f)
53 #define Biddy_GetThen(f) Cudd_T(f)
54 #define Biddy_AddVariable() Cudd_bddNewVar(manager)
55 #define Biddy_Not(f) Cudd_Not(f)
56 #define Biddy_Inv(f) Cudd_Not(f)
57 #define Biddy_And(f,g) Cudd_bddAnd(manager,f,g)
58 #define Biddy_Or(f,g) Cudd_bddOr(manager,f,g)
59 #define Biddy_Xnor(f,g) Cudd_bddXnor(manager,f,g)
60 #define Biddy_Support(f) Cudd_Support(manager,f)
61 #define Biddy_DependentVariableNumber(f) Cudd_SupportSize(manager,f)
62 #define Biddy_CountMinterm(f,n) Cudd_CountMinterm(manager,f,n)
63 #define Biddy_NodeNumber(f) Cudd_DagSize(f)
64 #define Biddy_PrintInfo(s) Cudd_PrintInfo(manager,s)
65 #endif
66 
67 extern void setDataUSA(unsigned int *size, unsigned int ***usa, unsigned int **order, char **codes);
68 extern void setDataEurope(unsigned int *size, unsigned int ***europe, unsigned int **order, char **codes);
69 static void createGraph(unsigned int size, unsigned int **edge, Biddy_Edge *state, Biddy_Edge *graph);
70 static Biddy_Edge calculateIndependence(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph);
71 static Biddy_Edge calculateKernels(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph);
72 static void writeOrder(Biddy_Edge f, char *codes, unsigned int *order, unsigned int size);
73 
74 int main(int argc, char** argv) {
75  unsigned int i;
76  Biddy_Boolean complete;
77  Biddy_Edge tmp;
78  Biddy_Edge r1,r2;
79  unsigned int n1,n2;
80  char *userinput;
81 
82 #ifdef USA_YES
83  unsigned int usaSize = 0;
84  unsigned int **usaEdge;
85  unsigned int *usaOrder;
86  char *usaCodes;
87  Biddy_Edge *usaState;
88  Biddy_Edge *usaGraph;
89 #endif
90 
91 #ifdef EUROPE_YES
92  unsigned int europeSize = 0;
93  unsigned int **europeEdge;
94  unsigned int *europeOrder;
95  char *europeCodes;
96  Biddy_Edge *europeState;
97  Biddy_Edge *europeGraph;
98 #endif
99 
100  setbuf(stdout, NULL);
101 
102 #ifdef USA_YES
103  setDataUSA(&usaSize,&usaEdge,&usaOrder,&usaCodes);
104 #endif
105 
106 #ifdef EUROPE_YES
107  setDataEurope(&europeSize,&europeEdge,&europeOrder,&europeCodes);
108 #endif
109 
110 #ifdef USE_BIDDY
111  /* There is only one unique table in Biddy */
112  /* There are three caches in Biddy */
113  /* Unique table grows over the time */
114  /* The max number of variables is hardcoded in biddyInt. h */
115  /* biddyVariableTable.usaSize = BIDDYVARMAX = 2048 */
116  /* The following constants are hardcoded in biddyMain.c */
117  /* biddyIteCache.usaSize = MEDIUM_TABLE = 262143 */
118  /* biddyEACache.usaSize = SMALL_TABLE = 65535 */
119  /* biddyRCCache.usaSize = SMALL_TABLE = 65535 */
120  /* DEFAULT INIT CALL: Biddy_InitAnonymous(BIDDYTYPEOBDD) */
121  Biddy_InitAnonymous(BIDDYTYPEOBDD);
122 #endif
123 
124 #ifdef USE_CUDD
125  /* In CUDD each variable has its own subtable in the unique table */
126  /* There is only one cache in CUDD */
127  /* Subtables grow over the time, you can set limit for fast unique table growth */
128  /* Cudd_SetLooseUpTo(manager,1048576) */
129  /* Cache can grow over the time, you can set the max usaSize */
130  /* Cudd_SetMaxCacheHard(manager,262144) */
131  /* These two constants are hardcoded in v3.0.0 */
132  /* CUDD_UNIQUE_SLOTS = 256 (default initial usaSize of each subtable) */
133  /* CUDD_CACHE_SLOTS = 262144 (default initial usaSize of cache table) */
134  /* DEFAULT INIT CALL: Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0) */
135  manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
136  Cudd_SetMaxCacheHard(manager,262144);
137 #endif
138 
139 #ifdef USA_YES
140  usaGraph = (Biddy_Edge *) malloc(usaSize*sizeof(Biddy_Edge *));
141  usaState = (Biddy_Edge *) malloc(usaSize*sizeof(Biddy_Edge *));
142 #endif
143 
144 #ifdef EUROPE_YES
145  europeGraph = (Biddy_Edge *) malloc(europeSize*sizeof(Biddy_Edge *));
146  europeState = (Biddy_Edge *) malloc(europeSize*sizeof(Biddy_Edge *));
147 #endif
148 
149  i = 0;
150  complete = FALSE;
151  while (!complete) {
152  complete = TRUE;
153  tmp = Biddy_AddVariable();
154 #ifdef USA_YES
155  if (i < usaSize) {
156  usaState[usaOrder[i]] = tmp;
157  }
158  complete = complete && (i >= (usaSize-1));
159 #endif
160 #ifdef EUROPE_YES
161  if (i < europeSize) {
162  europeState[europeOrder[i]] = tmp;
163  }
164  complete = complete && (i >= (europeSize-1));
165 #endif
166  i++;
167  }
168 
169 #ifdef USA_YES
170  createGraph(usaSize,usaEdge,usaState,usaGraph);
171 #endif
172 
173 #ifdef EUROPE_YES
174  createGraph(europeSize,europeEdge,europeState,europeGraph);
175 #endif
176 
177 #ifdef USE_BIDDY
178  Biddy_Clean();
179 #endif
180 
181  r1 = Biddy_GetConstantZero();
182  r2 = Biddy_GetConstantZero();
183 #ifdef USE_CUDD
184  Cudd_Ref(r1);
185  Cudd_Ref(r2);
186 #endif
187 
188 #ifdef USA_YES
189  if (!CALCULATE_KERNELS) {
190  /* CALCULATING INDEPENDENCE SETS FOR USA */
191 #ifdef USE_CUDD
192  Cudd_RecursiveDeref(manager,r1);
193 #endif
194  r1 = calculateIndependence(usaSize,usaState,usaGraph);
195  } else {
196  /* CALCULATING KERNELS (MAXIMUM INDEPENDENCE SETS) FOR USA */
197 #ifdef USE_CUDD
198  Cudd_RecursiveDeref(manager,r1);
199 #endif
200  r1 = calculateKernels(usaSize,usaState,usaGraph);
201  }
202 #ifdef USE_BIDDY
203  Biddy_AddPersistentFormula((Biddy_String)"usa",r1);
204  Biddy_Clean();
205 #endif
206 #ifdef USE_CUDD
207  for (i=0; i<usaSize; i++) {
208  Cudd_RecursiveDeref(manager,usaGraph[i]);
209  }
210 #endif
211 #endif
212 
213 #ifdef EUROPE_YES
214  if (!CALCULATE_KERNELS) {
215  /* CALCULATING INDEPENDENCE SETS FOR EUROPE */
216 #ifdef USE_CUDD
217  Cudd_RecursiveDeref(manager,r2);
218 #endif
219  r2 = calculateIndependence(europeSize,europeState,europeGraph);
220  } else {
221  /* CALCULATING KERNELS (MAXIMUM INDEPENDENCE SETS) FOR EUROPE */
222 #ifdef USE_CUDD
223  Cudd_RecursiveDeref(manager,r2);
224 #endif
225  r2 = calculateKernels(europeSize,europeState,europeGraph);
226  }
227 #ifdef USE_BIDDY
228  Biddy_AddPersistentFormula((Biddy_String)"europe",r2);
229  Biddy_Clean();
230 #endif
231 #ifdef USE_CUDD
232  for (i=0; i<europeSize; i++) {
233  Cudd_RecursiveDeref(manager,europeGraph[i]);
234  }
235 #endif
236 #endif
237 
238  userinput = strdup("...");
239  while (userinput[0] != 'x') {
240 
241  /* We have problems with passing stdout in the case you compile this file */
242  /* with MINGW and use biddy.dll generated with Visual Studio. */
243  /* In such cases, please, use Biddy_PrintInfo(NULL) */
244  if (userinput[0] == 'r') Biddy_PrintInfo(stdout);
245 
246  /* SIFTING */
247 #ifdef USE_BIDDY
248 #ifdef CONVERGE
249  if (userinput[0] == 's') Biddy_Sifting(NULL,TRUE);
250 #ifdef USA_YES
251  if (userinput[0] == 'u') Biddy_Sifting(r1,TRUE);
252 #endif
253 #ifdef EUROPE_YES
254  if (userinput[0] == 'e') Biddy_Sifting(r2,TRUE);
255 #endif
256 #else
257  if (userinput[0] == 's') Biddy_Sifting(NULL,FALSE);
258 #ifdef USA_YES
259  if (userinput[0] == 'u') Biddy_Sifting(r1,FALSE);
260 #endif
261 #ifdef EUROPE_YES
262  if (userinput[0] == 'e') Biddy_Sifting(r2,FALSE);
263 #endif
264 #endif
265 #endif
266 #ifdef USE_CUDD
267 #ifdef CONVERGE
268  if (userinput[0] == 's') Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT_CONVERGE,0);
269 #else
270  if (userinput[0] == 's') Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT,0);
271 #endif
272 #endif
275  if ((userinput[0] == 's')
276 #ifdef USA_YES
277  || (userinput[0] == 'u')
278 #endif
279 #ifdef EUROPE_YES
280  || (userinput[0] == 'e')
281 #endif
282  ) {
283 #ifdef CONVERGE
284  printf("(CONVERGING SIFTING");
285 #ifdef USE_BIDDY
286  if (userinput[0] == 'u') {
287  printf(" ON FUNCTION FOR USA");
288  }
289  if (userinput[0] == 'e') {
290  printf(" ON FUNCTION FOR EUROPE");
291  }
292 #endif
293  printf(") ");
294 #else
295  printf("(SIFTING");
296 #ifdef USE_BIDDY
297  if (userinput[0] == 'u') {
298  printf(" ON FUNCTION FOR USA");
299  }
300  if (userinput[0] == 'e') {
301  printf(" ON FUNCTION FOR EUROPE");
302  }
303 #endif
304  printf(") ");
305 #endif
306  }
307 
308  printf("Resulting function r1/r2 depends on %u/%u variables.\n",n1,n2);
309  printf("Resulting function r1/r2 has %.0f/%.0f minterms.\n",Biddy_CountMinterm(r1,n1),Biddy_CountMinterm(r2,n2));
310 #ifdef USE_BIDDY
311  printf("BDD for resulting function r1/r2 has %u/%u nodes (%u/%u nodes if using complement edges).\n",
313 #endif
314 #ifdef USE_CUDD
315  printf("BDD for resulting function r1/r2 has %u/%u nodes (using complement edges).\n",Biddy_NodeNumber(r1),Biddy_NodeNumber(r2));
316 #endif
317 #ifdef USE_BIDDY
318  printf("Variable swaps performed so far: %u\n",Biddy_NodeTableSwapNumber());
319 #endif
320 #ifdef USE_CUDD
321  printf("Variable swaps performed so far: %.0f\n",Cudd_ReadSwapSteps(manager));
322 #endif
323 #ifdef USA_YES
324  printf("Order for USA: ");
325  writeOrder(r1,usaCodes,usaOrder,usaSize);
326 #endif
327 #ifdef EUROPE_YES
328  printf("Order for Europe: ");
329  writeOrder(r2,europeCodes,europeOrder,europeSize);
330 #endif
331 #ifdef USE_BIDDY
332  printf("E[x]it or [r]eport or ");
333 #ifdef CONVERGE
334  printf("Converging sifting ");
335 #else
336  printf("Sifting ");
337 #endif
338 #if (defined USA_YES) || (defined EUROPE_YES)
339  printf("on [s]ystem or on function for");
340 #ifdef USA_YES
341  printf(" [u]SA");
342 #endif
343 #ifdef EUROPE_YES
344  printf(" [e]urope");
345 #endif
346 #endif
347  printf(": ");
348 #ifdef DOPROFILE
349  if (!strcmp(userinput,"r")) userinput = strdup("x");
350  if (!strcmp(userinput,"s")) userinput = strdup("r");
351  if (!strcmp(userinput,"...")) userinput = strdup("s");
352  printf("DOPROFILE\n");
353 #else
354  if (!scanf("%s",userinput)) printf("ERROR\n");
355 #endif
356 #endif
357 #ifdef USE_CUDD
358  printf("E[x]it or [r]eport or ");
359 #ifdef CONVERGE
360  printf("Converging sifting ");
361 #else
362  printf("Sifting ");
363 #endif
364  printf("on [s]ystem");
365  printf(": ");
366 #ifdef DOPROFILE
367  if (!strcmp(userinput,"r")) userinput = strdup("x");
368  if (!strcmp(userinput,"s")) userinput = strdup("r");
369  if (!strcmp(userinput,"...")) userinput = strdup("s");
370  printf("DOPROFILE\n");
371 #else
372  if (!scanf("%s",userinput)) printf("ERROR\n");
373 #endif
374 #endif
375  }
376 
377  free(userinput);
378 
379  /* EXIT */
380 #ifdef USE_BIDDY
381  Biddy_Exit();
382 #endif
383 #ifdef USE_CUDD
384  Cudd_RecursiveDeref(manager,r1);
385  Cudd_RecursiveDeref(manager,r2);
386  printf("CUDD: nodes with non-zero reference counts: %d\n",Cudd_CheckZeroRef(manager));
387  Cudd_Quit(manager);
388 #endif
389 
390  return 0;
391 }
392 
393 /* CREATE GRAPH */
394 static void createGraph(unsigned int size, unsigned int **edge, Biddy_Edge *state, Biddy_Edge *graph) {
395  unsigned int i,j;
396  Biddy_Edge tmp;
397  printf("CREATE GRAPH... ");
398  for (i=0; i<size; i++) {
399  graph[i] = Biddy_GetConstantZero();
400 #ifdef USE_CUDD
401  Cudd_Ref(graph[i]);
402 #endif
403  for (j=0; j<size; j++) {
404  if (edge[i][j]) {
405  tmp = Biddy_Or(graph[i],state[j]);
406 #ifdef USE_CUDD
407  Cudd_Ref(tmp);
408  Cudd_RecursiveDeref(manager,graph[i]);
409 #endif
410  graph[i] = tmp;
411  }
412  }
413 #ifdef USE_BIDDY
414  Biddy_AddTmpFormula(graph[i],0); /* permanently preserved */
415 #endif
416  }
417  printf("OK\n");
418 }
419 
420 /* CALCULATE INDEPENDENCE SETS */
421 static Biddy_Edge calculateIndependence(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph) {
422  unsigned int i;
423  Biddy_Edge p,r,tmp;
424  printf("CALCULATE INDEPENDENCE SETS...\n");
425  r = Biddy_GetConstantZero();
426 #ifdef USE_CUDD
427  Cudd_Ref(r);
428 #endif
429  for (i=0; i<size; i++) {
430  p = Biddy_And(graph[i],state[i]);
431 #ifdef USE_CUDD
432  Cudd_Ref(p);
433 #endif
434  tmp = Biddy_Or(r,p);
435 #ifdef USE_BIDDY
436  Biddy_AddTmpFormula(tmp,1);
437  Biddy_Clean();
438 #endif
439 #ifdef USE_CUDD
440  Cudd_Ref(tmp);
441  Cudd_RecursiveDeref(manager,r);
442  Cudd_RecursiveDeref(manager,p);
443  /* Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT,0); */
444 #endif
445  r = tmp;
446 #ifdef USE_BIDDY
447  /* Biddy_Sifting(NULL,FALSE); */
448  /* Biddy_Sifting(r,FALSE); */
449 #endif
450  }
451  return Biddy_Inv(r);
452 }
453 
454 /* CALCULATE KERNELS (MAXIMUM INDEPENDENCE SETS) */
455 static Biddy_Edge calculateKernels(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph) {
456  unsigned int i;
457  Biddy_Edge p,r,tmp;
458  printf("CALCULATE KERNELS (MAXIMUM INDEPENDENCE SETS)...\n");
459  r = Biddy_GetConstantZero();
460 #ifdef USE_CUDD
461  Cudd_Ref(r);
462 #endif
463  for (i=0; i<size; i++) {
464  p = Biddy_Xnor(graph[i],state[i]);
465 #ifdef USE_CUDD
466  Cudd_Ref(p);
467 #endif
468  tmp = Biddy_Or(r,p);
469 #ifdef USE_BIDDY
470  Biddy_AddTmpFormula(tmp,1);
471  Biddy_Clean();
472 #endif
473 #ifdef USE_CUDD
474  Cudd_Ref(tmp);
475  Cudd_RecursiveDeref(manager,r);
476  Cudd_RecursiveDeref(manager,p);
477  /* Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT,0); */
478 #endif
479  r = tmp;
480 #ifdef USE_BIDDY
481  /* Biddy_Sifting(NULL,FALSE); */
482  /* Biddy_Sifting(r,FALSE); */
483 #endif
484  }
485  return Biddy_Inv(r);
486 }
487 
488 static void writeOrder(Biddy_Edge f, char *codes, unsigned int *order, unsigned int size) {
489  char ch;
490 #ifdef USE_CUDD
491  int i, j;
492 #endif
493  int k;
494  unsigned int ivar = 0;
495 
496 #ifdef USE_BIDDY
497  /* TO DO: IMPLEMENT Biddy_ReadPerm() AND ITS INVERSE */
498  {
499  Biddy_Edge tmp;
500  tmp = Biddy_Support(f);
501  while (!Biddy_IsConstant(tmp)) {
502  /* In Biddy, the first user variable is at index [1] */
503  ivar = Biddy_GetTopVariable(tmp)-1;
504  k = 3*(order[ivar]);
505  ch = codes[k+2];
506  codes[k+2] = 0;
507  printf("%s",&codes[k]);
508  codes[k+2] = ch;
509  tmp = Biddy_GetThen(tmp);
510  if (!Biddy_IsConstant(tmp)) printf(","); else printf("\n");
511  }}
512 #endif
513 
514 #ifdef USE_CUDD
515  /* HOW TO AVOID THIS DOUBLE LOOP ??? */
516  for (i=0; i<size; i++) {
517  /* In CUDD, the first user variable is at index [0] */
518  for (j=0; j<size; j++) {
519  if (i == Cudd_ReadPerm(manager,j)) ivar = j;
520  }
521  k = 3 * (order[ivar]);
522  ch = codes[k + 2];
523  codes[k + 2] = 0;
524  printf("%s", &codes[k]);
525  codes[k + 2] = ch;
526  if (i != (size-1)) printf(","); else printf("\n");
527  }
528 #endif
529 
530 }
#define Biddy_CountMinterm(f, nvars)
Definition: biddy.h:905
void * Biddy_Edge
Definition: biddy.h:221
#define Biddy_And(f, g)
Definition: biddy.h:478
#define Biddy_Sifting(f, c)
Definition: biddy.h:689
#define Biddy_Clean()
Definition: biddy.h:620
#define Biddy_Xnor(f, g)
Definition: biddy.h:508
Biddy_Edge Biddy_GetThen(Biddy_Edge fun)
Function Biddy_GetThen returns THEN successor.
Definition: biddyMain.c:988
Biddy_Variable Biddy_GetTopVariable(Biddy_Edge fun)
Function Biddy_GetTopVariable returns the top variable.
Definition: biddyMain.c:1060
#define Biddy_DependentVariableNumber(f)
Definition: biddy.h:890
#define Biddy_Inv(f)
Definition: biddy.h:160
#define Biddy_NodeNumberPlain(f)
Definition: biddy.h:885
#define Biddy_PrintInfo(f)
Definition: biddy.h:927
#define Biddy_Or(f, g)
Definition: biddy.h:486
#define Biddy_NodeNumber(f)
Definition: biddy.h:735
#define Biddy_NodeTableSwapNumber()
Definition: biddy.h:790
#define Biddy_GetConstantZero()
Definition: biddy.h:340
#define Biddy_Exit()
Definition: biddy.h:272
File biddy.h contains declaration of all external data structures.
#define Biddy_Support(f)
Definition: biddy.h:582
char Biddy_Boolean
Definition: biddy.h:191
#define Biddy_IsConstant(f)
Definition: biddy.h:130
char * Biddy_String
Definition: biddy.h:194