Biddy  1.7.1
An academic Binary Decision Diagrams package
biddy-example-8queens.c
1 /* $Revision: 253 $ */
2 /* $Date: 2017-03-20 09:03:47 +0100 (pon, 20 mar 2017) $ */
3 /* This file (biddy-example-8queens.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 -DREPORT -DEVENTLOG_NONE -DUSE_BIDDY -DUNIX -O2 -o biddy-example-8queens biddy-example-8queens.c -I. -L./bin -lbiddy -lgmp */
11 /* gcc -DREPORT -DEVENTLOG_NONE -DUSE_CUDD -O2 -o cudd-example-8queens biddy-example-8queens.c -I ../cudd/include/ -L ../cudd/lib/ -lcudd -lm */
12 
13 /* to enable the 1993 edition of the POSIX.1b standard (IEEE Standard 1003.1b-1993) */
14 /* #define _POSIX_C_SOURCE (199309L) */
15 
16 /* default size, this can be overriden via argument */
17 #define SIZE 8
18 #define USE_GARBAGE_COLLECTION
19 
20 /* for BIDDY there are 3 variants possible: */
21 /* NOT_USE_SIFTING, USE_SIFTING, USE_SIFTING_R */
22 #define NOT_USE_SIFTING
23 
24 /* there are 5 variants possible */
25 /* NOT_POSTPONE, POSTPONE_FIFO, POSTPONE_LIFO, POSTPONE_REVERSE_FIFO, POSTPONE_REVERSE_LIFO */
26 #define NOT_POSTPONE
27 
28 /* event log (EVENTLOG_TIME, EVENTLOG_SIZE, or EVENTLOG_RESULT) */
29 #ifdef EVENTLOG_TIME
30 # define ZF_LOGI(x) {static unsigned int zfstat = 0;printf(x);printf("#%u,%.2f\n",++zfstat,clock()/(1.0*CLOCKS_PER_SEC));}
31 #endif
32 #ifdef EVENTLOG_SIZE
33 # ifdef USE_BIDDY
34 # define ZF_LOGI(x) {static unsigned int zfstat = 0;printf(x);printf("#%u,%u,%u\n",++zfstat,Biddy_NodeTableNum(),Biddy_NodeTableSize());}
35 # endif
36 # ifdef USE_CUDD
37 # define ZF_LOGI(x) {static unsigned int zfstat = 0;printf(x);printf("#%u,%u,%u\n",++zfstat,Cudd_ReadKeys(manager),Cudd_ReadSlots(manager));}
38 # endif
39 #endif
40 #ifdef EVENTLOG_RESULT
41 # ifdef USE_BIDDY
42 # define ZF_LOGI(x) {static unsigned int zfstat = 0;printf(x);printf("#%u,%u\n",++zfstat,Biddy_NodeNumber(r));}
43 # endif
44 # ifdef USE_CUDD
45 # define ZF_LOGI(x) {static unsigned int zfstat = 0;printf(x);printf("#%u,%u\n",++zfstat,Cudd_DagSize(r));}
46 # endif
47 #endif
48 #ifndef ZF_LOGI
49 # define ZF_LOGI(x)
50 #endif
51 
52 #ifdef USE_BIDDY
53 # include "biddy.h"
54 # define BDDNULL NULL
55 /* #define Biddy_Inv(f) Biddy_NOT(f) */ /* for compatibility with Biddy v1.6 */
56 #endif
57 
58 #ifdef USE_CUDD
59 # include <stdio.h>
60 # include <stdlib.h>
61 # include <stdint.h>
62 # include <string.h>
63 # include <ctype.h>
64 # include <stdarg.h>
65 # include <math.h>
66 # include "cudd.h"
67 # define BDDNULL NULL
68 # ifndef TRUE
69 # define TRUE (0 == 0)
70 # endif
71 # ifndef FALSE
72 # define FALSE !TRUE
73 # endif
74 typedef char *Biddy_String;
75 typedef char Biddy_Boolean;
76 typedef DdNode *Biddy_Edge;
77 DdManager *manager;
78 #endif
79 
80 #include <time.h>
81 
82 #ifdef USE_CUDD
83 #define BIDDYTYPEOBDD 1
84 #define BIDDYTYPEZBDD 2
85 #define BIDDYTYPETZBDD 3
86 #define Biddy_GetManagerType() BIDDYTYPEOBDD
87 #define Biddy_GetConstantZero() Cudd_ReadLogicZero(manager)
88 #define Biddy_GetConstantOne() Cudd_ReadOne(manager)
89 #define Biddy_AddVariable() Cudd_bddNewVar(manager)
90 #define Biddy_Inv(f) Cudd_Not(f)
91 #define Biddy_Not(f) Cudd_Not(f)
92 #define Biddy_And(f,g) Cudd_bddAnd(manager,f,g)
93 #define Biddy_Or(f,g) Cudd_bddOr(manager,f,g)
94 #define Biddy_Xor(f,g) Cudd_bddXor(manager,f,g)
95 #define Biddy_DependentVariableNumber(f) Cudd_SupportSize(manager,f)
96 #define Biddy_CountMinterm(f,n) Cudd_CountMinterm(manager,f,n)
97 #define Biddy_DensityBDD(f,n) Cudd_Density(manager,f,n)
98 #define Biddy_NodeNumber(f) Cudd_DagSize(f)
99 #define Biddy_PrintInfo(s) Cudd_PrintInfo(manager,s)
100 #define Biddy_NodeTableNum() Cudd_ReadKeys(manager)
101 #define Biddy_NodeTableSize() Cudd_ReadSlots(manager)
102 #define Biddy_ReadMemoryInUse() Cudd_ReadMemoryInUse(manager)
103 #endif
104 
105 void checkOutOfLimits(unsigned int size, clock_t elapsedtime) {
106 #ifdef USE_BIDDY
107  if ((size == 9) && (Biddy_ReadMemoryInUse() > 120000000)) {
108  fprintf(stderr,"9, -1, -1, -1\n");
109  exit(1);
110  }
111  if ((size == 10) && (Biddy_NodeTableSize() > 4194304)) {
112  fprintf(stderr,"10, -1, -1, -1\n");
113  exit(1);
114  }
115  if ((size == 10) && (Biddy_ReadMemoryInUse() > 300000000)) {
116  fprintf(stderr,"10, -1, -1, -1\n");
117  exit(1);
118  }
119 /*
120  if ((size == 10) && ((clock()-elapsedtime)/(1.0*CLOCKS_PER_SEC) > 120.0)) {
121  fprintf(stderr,"10, -1, -1, -1\n");
122  exit(1);
123  }
124 */
125 #endif
126 }
127 
128 int main(int argc, char** argv) {
129  unsigned int i,j,k,n,size,seq,seq1;
130  Biddy_Edge **board;
131  Biddy_Edge tmp;
132  Biddy_Edge t,r;
133  Biddy_Edge *fifo1,*LP1;
134  Biddy_Edge *fifo2,*LP2;
135 
136  clock_t elapsedtime;
137  /* struct timespec elapsedtimex, stoptimex; */
138 
139  elapsedtime = clock();
140  /* if (clock_gettime(CLOCK_PROCESS_CPUTIME_ID,&elapsedtimex) == -1) printf("ERROR WITH clock_gettime!\n"); */
141 
142  if (argc > 1) {
143  sscanf(argv[1],"%u",&size);
144  } else {
145  size = SIZE;
146  }
147 
148  if ((size < 2) || (size > 15)) {
149  printf("WRONG SIZE!\n");
150  exit(1);
151  }
152 
153  setbuf(stdout, NULL);
154 
155  LP1 = fifo1 = (Biddy_Edge *) malloc((4 * size * size + size) * sizeof(Biddy_Edge));
156  LP2 = fifo2 = (Biddy_Edge *) malloc((4 * size * size + size) * sizeof(Biddy_Edge));
157  LP1--;
158 
159 #ifdef USE_BIDDY
160  seq = 0;
161 #endif
162 
163  board = (Biddy_Edge **) malloc((size+1)*sizeof(Biddy_Edge *));
164  for (i=0; i<=size; i++) {
165  board[i] = (Biddy_Edge *) malloc((size+1)*sizeof(Biddy_Edge));
166  }
167 
168 #ifdef USE_BIDDY
169  /* There is only one unique table in Biddy */
170  /* There are three caches in Biddy */
171  /* New nodes are added in blocks */
172  /* The max number of variables is hardcoded in biddyInt. h */
173  /* biddyVariableTable.size = BIDDYVARMAX = 2048 */
174  /* The following constants are hardcoded in biddyMain.c */
175  /* biddyNodeTable.size = BIG_TABLE = 1048575 */
176  /* biddyIteCache.size = MEDIUM_TABLE = 262143 */
177  /* biddyEACache.size = SMALL_TABLE = 65535 */
178  /* biddyRCCache.size = SMALL_TABLE = 65535 */
179  /* biddyBlockSize = 524288 */
180  /* DEFAULT INIT CALL: Biddy_InitAnonymous(BIDDYTYPEOBDD) */
181  Biddy_InitAnonymous(BIDDYTYPEOBDD);
182  if (argc == 2) {
183  Biddy_SetManagerParameters(-1,-1,-1,-1,-1,-1,-1,-1,-1,-1);
184  }
185  else if (argc == 8) {
186  unsigned int gcr,gcrF,gcrX;
187  unsigned int rr,rrF,rrX;
188  sscanf(argv[2],"%u",&gcr);
189  sscanf(argv[3],"%u",&gcrF);
190  sscanf(argv[4],"%u",&gcrX);
191  sscanf(argv[5],"%u",&rr);
192  sscanf(argv[6],"%u",&rrF);
193  sscanf(argv[7],"%u",&rrX);
194  Biddy_SetManagerParameters(gcr/100.0,gcrF/100.0,gcrX/100.0,rr/100.0,rrF/100.0,rrX/100.0,-1,-1,-1,-1);
195  }
196  else if (argc == 12) {
197  unsigned int gcr,gcrF,gcrX;
198  unsigned int rr,rrF,rrX;
199  unsigned int st;
200  unsigned int fst;
201  unsigned int cst;
202  unsigned int fcst;
203  sscanf(argv[2],"%u",&gcr);
204  sscanf(argv[3],"%u",&gcrF);
205  sscanf(argv[4],"%u",&gcrX);
206  sscanf(argv[5],"%u",&rr);
207  sscanf(argv[6],"%u",&rrF);
208  sscanf(argv[7],"%u",&rrX);
209  sscanf(argv[8],"%u",&st);
210  sscanf(argv[9],"%u",&fst);
211  sscanf(argv[10],"%u",&cst);
212  sscanf(argv[11],"%u",&fcst);
213  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);
214  }
215  else {
216  printf("Wrong number of parameters!\n");
217  printf("USAGE (short): biddy-example-8queens SIZE GCR GCRF GCRX RR RRF RRX\n");
218  printf("USAGE (long): biddy-example-8queens SIZE GCR GCRF GCRX RR RRF RRX ST FST CST FCST\n");
219  printf("All parameters should be integer numbers >= 0");
220  exit(1);
221  }
222 #endif
223 
224 #ifdef USE_CUDD
225  /* In CUDD each variable has its own subtable in the unique table */
226  /* There is only one cache in CUDD */
227  /* Subtables grow over the time, you can set limit for fast unique table growth */
228  /* Cudd_SetLooseUpTo(manager,1048576) */
229  /* Cache can grow over the time, you can set the max size */
230  /* Cudd_SetMaxCacheHard(manager,262144) */
231  /* These two constants are hardcoded in v3.0.0 */
232  /* CUDD_UNIQUE_SLOTS = 256 (default initial size of each subtable) */
233  /* CUDD_CACHE_SLOTS = 262144 (default initial size of cache table) */
234  /* DEFAULT INIT CALL: Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0) */
235  manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
236  Cudd_SetMaxCacheHard(manager,262144);
237 #ifndef USE_GARBAGE_COLLECTION
238  Cudd_DisableGarbageCollection(manager);
239 #endif
240 #endif
241 
242  for (i=1; i<=size; i++) {
243  board[0][i] = board[i][0] = NULL;
244  }
245 
246  for (i=1; i<=size; i++) {
247  for (j=1; j<=size; j++) {
248  board[i][j] = Biddy_AddVariable();
249  }
250  }
251 
252  /* for ZBDDs, by adding new variables all the existing ones are changed */
253  /* after adding the last variable we have to refresh edges in v1 and v2 */
254  /* NOTE: user variables in Biddy start with index 1 */
255 #ifdef USE_BIDDY
256  if (Biddy_GetManagerType() == BIDDYTYPEZBDD) {
257  for (i=1; i<=size; i++) {
258  for (j=1; j<=size; j++) {
259  board[i][j] = Biddy_GetVariableEdge((i-1)*size+(j-1)+1);
260  }
261  }
262  }
263 #endif
264 
265  /* Alternatively, Biddy allows a solution with named variables */
266  /*
267  {
268  Biddy_String name;
269  name = malloc(7);
270  for (i=1; i<=size; i++) {
271  for (j=1; j<=size; j++) {
272  sprintf(name,"r%uc%u",i,j);
273  board[i][j] = Biddy_AddVariableByName(name);
274  }
275  }
276  if (Biddy_GetManagerType() == BIDDYTYPEZBDD) {
277  for (i=1; i<=size; i++) {
278  for (j=1; j<=size; j++) {
279  sprintf(name,"r%uc%u",i,j);
280  board[i][j] = Biddy_GetVariableEdge(Biddy_GetVariable(name));
281  }
282  }
283  }
284  free(name);
285  }
286  */
287 
288  r = Biddy_GetConstantOne();
289 #ifdef USE_CUDD
290  Cudd_Ref(r);
291 #endif
292 
293  ZF_LOGI("INIT");
294 
295  /* ROWS */
296 #ifdef REPORT
297  printf("\nSTARTING ROWS\n");
298 #endif
299  for (i=1; i<=size; i++) {
300 #ifdef REPORT
301  printf("(%d/%d)",i,size);
302 #endif
303  for (j=1; j<=size; j++) {
304  t = Biddy_GetConstantOne();
305 #ifdef USE_CUDD
306  Cudd_Ref(t);
307 #endif
308  for (k=1; k<=size; k++) {
309  if (k != j) {
310  ZF_LOGI("R_AND");
311  tmp = Biddy_And(t,Biddy_Not(board[i][k]));
312 #ifdef USE_CUDD
313  Cudd_Ref(tmp);
314  Cudd_RecursiveDeref(manager,t);
315 #endif
316  t = tmp;
317  }
318  }
319  ZF_LOGI("R_OR");
320  tmp = Biddy_Or(t,Biddy_Not(board[i][j]));
321 #ifdef NOT_POSTPONE
322 #ifdef USE_BIDDY
323 #ifdef USE_GARBAGE_COLLECTION
324  Biddy_AddTmpFormula(r,1);
325  Biddy_AddTmpFormula(tmp,1);
326  Biddy_Clean();
327 #endif
328 #endif
329 #endif
330 #ifdef USE_CUDD
331  Cudd_Ref(tmp);
332  Cudd_RecursiveDeref(manager,t);
333 #endif
334  t = tmp;
335 
336  /* FREQUENT GC CALLS SEEMS TO BE BENEFICIAL FOR THIS EXAMPLE */
337 #ifdef USE_BIDDY_X
338  Biddy_AutoGC();
339 #endif
340 
341 #ifdef NOT_POSTPONE
342  ZF_LOGI("R_AND");
343  tmp = Biddy_And(r,t);
344 #ifdef USE_BIDDY
345 #ifdef USE_GARBAGE_COLLECTION
346  Biddy_AddTmpFormula(tmp,1);
347  Biddy_Clean();
348 #endif
349 #endif
350 #ifdef USE_CUDD
351  Cudd_Ref(tmp);
352  Cudd_RecursiveDeref(manager,t);
353  Cudd_RecursiveDeref(manager,r);
354 #endif
355  r = tmp;
356 #else
357  *(++LP1) = t;
358 #endif
359 
360  ZF_LOGI("R_MEM");
361 
362 #ifdef USE_BIDDY
363 #ifdef USE_GARBAGE_COLLECTION
364 #ifdef POSTPONE_FIFO
365  seq++;
366  Biddy_AddTmpFormula(t,(seq-1)/2);
367 #endif
368 #ifdef POSTPONE_REVERSE_FIFO
369  seq++;
370  Biddy_AddTmpFormula(t,(4 * size * size + size - seq)/2);
371 #endif
372 #ifdef POSTPONE_LIFO
373  seq++;
374  if (seq == 1) {
375  Biddy_AddTmpFormula(t,seq-1);
376  } else {
377  Biddy_AddTmpFormula(t,seq-2);
378  }
379 #endif
380 #ifdef POSTPONE_REVERSE_LIFO
381  seq++;
382  Biddy_AddTmpFormula(t,(4 * size * size + size) - seq - 1);
383 #endif
384 #endif
385 #endif
386 
387  }
388  }
389 
390  /* EXPLICIT CALL TO GC AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
391 #ifdef USE_BIDDY_X
392  Biddy_AutoGC();
393 #endif
394 
395  /* PROFILING */
396  /*
397  checkOutOfLimits(size,elapsedtime);
398  */
399 
400  /* SIFTING AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
401  /* IT IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
402 #ifdef USE_BIDDY
403 #ifdef NOT_POSTPONE
404 #ifdef USE_SIFTING
405  ZF_LOGI("R_SIFT");
406  Biddy_Sifting(NULL,FALSE);
407 #endif
408 #ifdef USE_SIFTING_R
409  ZF_LOGI("R_SIFT_R");
410  Biddy_Sifting(r,FALSE);
411 #endif
412 #endif
413 #endif
414 
415  /* COLUMNS */
416 #ifdef REPORT
417  printf("\nSTARTING COLUMNS\n");
418 #endif
419  for (i=1; i<=size; i++) {
420 #ifdef REPORT
421  printf("(%d/%d)",i,size);
422 #endif
423  for (j=1; j<=size; j++) {
424  t = Biddy_GetConstantOne();
425 #ifdef USE_CUDD
426  Cudd_Ref(t);
427 #endif
428  for (k=1; k<=size; k++) {
429  if (k != i) {
430  ZF_LOGI("C_AND");
431  tmp = Biddy_And(t,Biddy_Not(board[k][j]));
432 #ifdef USE_CUDD
433  Cudd_Ref(tmp);
434  Cudd_RecursiveDeref(manager,t);
435 #endif
436  t = tmp;
437  }
438  }
439  ZF_LOGI("C_OR");
440  tmp = Biddy_Or(t,Biddy_Not(board[i][j]));
441 #ifdef NOT_POSTPONE
442 #ifdef USE_BIDDY
443 #ifdef USE_GARBAGE_COLLECTION
444  Biddy_AddTmpFormula(r,1);
445  Biddy_AddTmpFormula(tmp,1);
446  Biddy_Clean();
447 #endif
448 #endif
449 #endif
450 #ifdef USE_CUDD
451  Cudd_Ref(tmp);
452  Cudd_RecursiveDeref(manager,t);
453 #endif
454  t = tmp;
455 
456  /* FREQUENT GC CALLS SEEMS TO BE BENEFICIAL FOR THIS EXAMPLE */
457 #ifdef USE_BIDDY_X
458  Biddy_AutoGC();
459 #endif
460 
461 #ifdef NOT_POSTPONE
462  ZF_LOGI("C_AND");
463  tmp = Biddy_And(r,t);
464 #ifdef USE_BIDDY
465 #ifdef USE_GARBAGE_COLLECTION
466  Biddy_AddTmpFormula(tmp,1);
467  Biddy_Clean();
468 #endif
469 #endif
470 #ifdef USE_CUDD
471  Cudd_Ref(tmp);
472  Cudd_RecursiveDeref(manager,t);
473  Cudd_RecursiveDeref(manager,r);
474 #endif
475  r = tmp;
476 #else
477  *(++LP1) = t;
478 #endif
479 
480  ZF_LOGI("C_MEM");
481 
482 #ifdef USE_BIDDY
483 #ifdef USE_GARBAGE_COLLECTION
484 #ifdef POSTPONE_FIFO
485  seq++;
486  Biddy_AddTmpFormula(t,(seq-1)/2);
487 #endif
488 #ifdef POSTPONE_REVERSE_FIFO
489  seq++;
490  Biddy_AddTmpFormula(t,(4 * size * size + size - seq)/2);
491 #endif
492 #ifdef POSTPONE_LIFO
493  seq++;
494  Biddy_AddTmpFormula(t,seq-2);
495 #endif
496 #ifdef POSTPONE_REVERSE_LIFO
497  seq++;
498  Biddy_AddTmpFormula(t,(4 * size * size + size) - seq - 1);
499 #endif
500 #endif
501 #endif
502 
503  }
504  }
505 
506  /* EXPLICIT CALL TO GC AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
507 #ifdef USE_BIDDY_X
508  Biddy_AutoGC();
509 #endif
510 
511  /* PROFILING */
512  /*
513  checkOutOfLimits(size,elapsedtime);
514  */
515 
516  /* SIFTING AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
517  /* IT IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
518 #ifdef USE_BIDDY
519 #ifdef NOT_POSTPONE
520 #ifdef USE_SIFTING
521  ZF_LOGI("C_SIFT");
522  Biddy_Sifting(NULL,FALSE);
523 #endif
524 #ifdef USE_SIFTING_R
525  ZF_LOGI("C_SIFT_R");
526  Biddy_Sifting(r,FALSE);
527 #endif
528 #endif
529 #endif
530 
531  /* RISING DIAGONALS */
532 #ifdef REPORT
533  printf("\nSTARTING RISING DIAGONALS\n");
534 #endif
535  for (i=1; i<=size; i++) {
536 #ifdef REPORT
537  printf("(%d/%d)",i,size);
538 #endif
539  for (j=1; j<=size; j++) {
540  t = Biddy_GetConstantOne();
541 #ifdef USE_CUDD
542  Cudd_Ref(t);
543 #endif
544  for (k=1; k<=size; k++) {
545  if ((j+k-i >= 1) && (j+k-i <= size) && (k != i)) {
546  ZF_LOGI("RD_AND");
547  tmp = Biddy_And(t,Biddy_Not(board[k][j+k-i]));
548 #ifdef USE_CUDD
549  Cudd_Ref(tmp);
550  Cudd_RecursiveDeref(manager,t);
551 #endif
552  t = tmp;
553  }
554  }
555  ZF_LOGI("RD_OR");
556  tmp = Biddy_Or(t,Biddy_Not(board[i][j]));
557 #ifdef NOT_POSTPONE
558 #ifdef USE_BIDDY
559 #ifdef USE_GARBAGE_COLLECTION
560  Biddy_AddTmpFormula(r,1);
561  Biddy_AddTmpFormula(tmp,1);
562  Biddy_Clean();
563 #endif
564 #endif
565 #endif
566 #ifdef USE_CUDD
567  Cudd_Ref(tmp);
568  Cudd_RecursiveDeref(manager,t);
569 #endif
570  t = tmp;
571 
572  /* FREQUENT GC CALLS SEEMS TO BE BENEFICIAL FOR THIS EXAMPLE */
573 #ifdef USE_BIDDY_X
574  Biddy_AutoGC();
575 #endif
576 
577 #ifdef NOT_POSTPONE
578  ZF_LOGI("RD_AND");
579  tmp = Biddy_And(r,t);
580 #ifdef USE_BIDDY
581 #ifdef USE_GARBAGE_COLLECTION
582  Biddy_AddTmpFormula(tmp,1);
583  Biddy_Clean();
584 #endif
585 #endif
586 #ifdef USE_CUDD
587  Cudd_Ref(tmp);
588  Cudd_RecursiveDeref(manager,t);
589  Cudd_RecursiveDeref(manager,r);
590 #endif
591  r = tmp;
592 #else
593  *(++LP1) = t;
594 #endif
595 
596  ZF_LOGI("RD_MEM");
597 
598 #ifdef USE_BIDDY
599 #ifdef USE_GARBAGE_COLLECTION
600 #ifdef POSTPONE_FIFO
601  seq++;
602  Biddy_AddTmpFormula(t,(seq-1)/2);
603 #endif
604 #ifdef POSTPONE_REVERSE_FIFO
605  seq++;
606  Biddy_AddTmpFormula(t,(4 * size * size + size - seq)/2);
607 #endif
608 #ifdef POSTPONE_LIFO
609  seq++;
610  Biddy_AddTmpFormula(t,seq-2);
611 #endif
612 #ifdef POSTPONE_REVERSE_LIFO
613  seq++;
614  Biddy_AddTmpFormula(t,(4 * size * size + size) - seq - 1);
615 #endif
616 #endif
617 #endif
618 
619  }
620  }
621 
622  /* EXPLICIT CALL TO GC AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
623 #ifdef USE_BIDDY_X
624  Biddy_AutoGC();
625 #endif
626 
627  /* PROFILING */
628  /*
629  checkOutOfLimits(size,elapsedtime);
630  */
631 
632  /* SIFTING AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
633  /* IT IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
634 #ifdef USE_BIDDY
635 #ifdef NOT_POSTPONE
636 #ifdef USE_SIFTING
637  ZF_LOGI("RD_SIFT");
638  Biddy_Sifting(NULL,FALSE);
639 #endif
640 #ifdef USE_SIFTING_R
641  ZF_LOGI("RD_SIFT_R");
642  Biddy_Sifting(r,FALSE);
643 #endif
644 #endif
645 #endif
646 
647  /* FALLING DIAGONALS */
648 #ifdef REPORT
649  printf("\nSTARTING FALLING DIAGONALS\n");
650 #endif
651  for (i=1; i<=size; i++) {
652 #ifdef REPORT
653  printf("(%d/%d)",i,size);
654 #endif
655  for (j=1; j<=size; j++) {
656  t = Biddy_GetConstantOne();
657 #ifdef USE_CUDD
658  Cudd_Ref(t);
659 #endif
660  for (k=1; k<=size; k++) {
661  if ((j+i-k >= 1) && (j+i-k <= size) && (k != i)) {
662  ZF_LOGI("FD_AND");
663  tmp = Biddy_And(t,Biddy_Not(board[k][j+i-k]));
664 #ifdef USE_CUDD
665  Cudd_Ref(tmp);
666  Cudd_RecursiveDeref(manager,t);
667 #endif
668  t = tmp;
669  }
670  }
671  ZF_LOGI("FD_OR");
672  tmp = Biddy_Or(t,Biddy_Not(board[i][j]));
673 #ifdef NOT_POSTPONE
674 #ifdef USE_BIDDY
675 #ifdef USE_GARBAGE_COLLECTION
676  Biddy_AddTmpFormula(r,1);
677  Biddy_AddTmpFormula(tmp,1);
678  Biddy_Clean();
679 #endif
680 #endif
681 #endif
682 #ifdef USE_CUDD
683  Cudd_Ref(tmp);
684  Cudd_RecursiveDeref(manager,t);
685 #endif
686  t = tmp;
687 
688  /* FREQUENT GC CALLS SEEMS TO BE BENEFICIAL FOR THIS EXAMPLE */
689 #ifdef USE_BIDDY_X
690  Biddy_AutoGC();
691 #endif
692 
693 #ifdef NOT_POSTPONE
694  ZF_LOGI("FD_AND");
695  tmp = Biddy_And(r,t);
696 #ifdef USE_BIDDY
697 #ifdef USE_GARBAGE_COLLECTION
698  Biddy_AddTmpFormula(tmp,1);
699  Biddy_Clean();
700 #endif
701 #endif
702 #ifdef USE_CUDD
703  Cudd_Ref(tmp);
704  Cudd_RecursiveDeref(manager,t);
705  Cudd_RecursiveDeref(manager,r);
706 #endif
707  r = tmp;
708 #else
709  *(++LP1) = t;
710 #endif
711 
712  ZF_LOGI("FD_MEM");
713 
714 #ifdef USE_BIDDY
715 #ifdef USE_GARBAGE_COLLECTION
716 #ifdef POSTPONE_FIFO
717  seq++;
718  Biddy_AddTmpFormula(t,(seq-1)/2);
719 #endif
720 #ifdef POSTPONE_REVERSE_FIFO
721  seq++;
722  Biddy_AddTmpFormula(t,(4 * size * size + size - seq)/2);
723 #endif
724 #ifdef POSTPONE_LIFO
725  seq++;
726  Biddy_AddTmpFormula(t,seq-2);
727 #endif
728 #ifdef POSTPONE_REVERSE_LIFO
729  seq++;
730  Biddy_AddTmpFormula(t,(4 * size * size + size) - seq - 1);
731 #endif
732 #endif
733 #endif
734 
735  }
736  }
737 
738  /* EXPLICIT CALL TO GC AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
739 #ifdef USE_BIDDY_X
740  Biddy_AutoGC();
741 #endif
742 
743  /* PROFILING */
744  /*
745  checkOutOfLimits(size,elapsedtime);
746  */
747 
748  /* SIFTING AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
749  /* IT IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
750 #ifdef USE_BIDDY
751 #ifdef NOT_POSTPONE
752 #ifdef USE_SIFTING
753  ZF_LOGI("FD_SIFT");
754  Biddy_Sifting(NULL,FALSE);
755 #endif
756 #ifdef USE_SIFTING_R
757  ZF_LOGI("FD_SIFT_R");
758  Biddy_Sifting(r,FALSE);
759 #endif
760 #endif
761 #endif
762 
763  /* THERE MUST BE A QUEEN IN EACH ROW */
764 #ifdef REPORT
765  printf("\nSTARTING FINAL CALCULATONS\n");
766 #endif
767  for (i=1; i<=size; i++) {
768 #ifdef REPORT
769  printf("(%d/%d)",i,size);
770 #endif
771  t = Biddy_GetConstantZero();
772 #ifdef USE_CUDD
773  Cudd_Ref(t);
774 #endif
775  for (j=1; j<=size; j++) {
776  ZF_LOGI("F_OR");
777  tmp = Biddy_Or(t,board[i][j]);
778 #ifdef USE_CUDD
779  Cudd_Ref(tmp);
780  Cudd_RecursiveDeref(manager,t);
781 #endif
782  t = tmp;
783  }
784 
785  /* FREQUENT GC CALLS SEEMS TO BE BENEFICIAL FOR THIS EXAMPLE */
786 #ifdef USE_BIDDY_X
787  Biddy_AutoGC();
788 #endif
789 
790 #ifdef NOT_POSTPONE
791  ZF_LOGI("F_AND");
792  tmp = Biddy_And(r,t);
793 #ifdef USE_BIDDY
794 #ifdef USE_GARBAGE_COLLECTION
795  Biddy_AddTmpFormula(tmp,1);
796  Biddy_Clean();
797 #endif
798 #endif
799 #ifdef USE_CUDD
800  Cudd_Ref(tmp);
801  Cudd_RecursiveDeref(manager,t);
802  Cudd_RecursiveDeref(manager,r);
803 #endif
804  r = tmp;
805 #else
806  *(++LP1) = t;
807 #endif
808 
809  ZF_LOGI("F_MEM");
810 
811 #ifdef USE_BIDDY
812 #ifdef USE_GARBAGE_COLLECTION
813 #ifdef POSTPONE_FIFO
814  seq++;
815  Biddy_AddTmpFormula(t,(seq-1)/2);
816  /* printf("(add %d)",(seq-1)/2); */
817 #endif
818 #ifdef POSTPONE_REVERSE_FIFO
819  seq++;
820  Biddy_AddTmpFormula(t,(4 * size * size + size - seq)/2);
821  /* printf("(add %d)",(4 * size * size + size - seq)/2); */
822 #endif
823 #ifdef POSTPONE_LIFO
824  seq++;
825  Biddy_AddTmpFormula(t,seq-2);
826  /* printf("(add %d)",seq-2); */
827 #endif
828 #ifdef POSTPONE_REVERSE_LIFO
829  seq++;
830  if (seq == (4 * size *size + size)) {
831  Biddy_AddTmpFormula(t,4 * size * size + size - seq);
832  /* printf("(add %d)",4 * size * size + size - seq); */
833  } else {
834  Biddy_AddTmpFormula(t,4 * size * size + size - seq - 1);
835  /* printf("(add %d)",4 * size * size + size - seq - 1); */
836  }
837 #endif
838 #endif
839 #endif
840 
841  /* PROFILING */
842  /*
843  checkOutOfLimits(size,elapsedtime);
844  */
845 
846  }
847 
848  /* EXPLICIT CALL TO GC AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
849 #ifdef USE_BIDDY_X
850  Biddy_AutoGC();
851 #endif
852 
853  /* PROFILING */
854  /*
855  checkOutOfLimits(size,elapsedtime);
856  */
857 
858  /* SIFTING AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
859  /* IT IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
860 #ifdef USE_BIDDY
861 #ifdef NOT_POSTPONE
862 #ifdef USE_SIFTING
863  ZF_LOGI("FD_SIFT");
864  Biddy_Sifting(NULL,FALSE);
865 #endif
866 #ifdef USE_SIFTING_R
867  ZF_LOGI("FD_SIFT_R");
868  Biddy_Sifting(r,FALSE);
869 #endif
870 #endif
871 #endif
872 
873  ZF_LOGI("P_MEM");
874 
875 /* POSTPONED ELEMENTS WILL BE CALCULATED IN REVERSED ORDER */
876 #if defined(POSTPONE_FIFO) || defined(POSTPONE_LIFO)
877  LP1++;
878  LP2 = fifo2;
879  LP2--;
880  while(LP1 != fifo1) {
881  *(++LP2) = *(--LP1);
882  }
883  fifo1 = fifo2;
884  fifo2 = LP1;
885  LP1 = LP2;
886 #endif
887 
888 #ifdef NOT_POSTPONE
889 #ifdef REPORT
890  printf("\nAnd OPERATIONS ARE NOT POSTPONED\n");
891 #endif
892 #endif
893 
894 /* POSTPONE And OPERATIONS USING FIFO */
895 #if defined(POSTPONE_FIFO) || defined(POSTPONE_REVERSE_FIFO)
896 #ifdef REPORT
897  printf("\nPOSTPONED And OPERATIONS USING FIFO\n");
898 #endif
899 #ifdef USE_CUDD
900  Cudd_RecursiveDeref(manager,r);
901 #endif
902  i = 0;
903  do {
904  LP1++;
905  LP2 = fifo2;
906  LP2--;
907  seq1 = (seq+1)/2;
908  seq = 0;
909  while(LP1 != fifo1) {
910  ZF_LOGI("P_MEM");
911  seq++;
912  r = *(--LP1);
913  if (LP1 == fifo1) {
914  *(++LP2) = r;
915 #ifdef USE_BIDDY
916 #ifdef USE_GARBAGE_COLLECTION
917  Biddy_AddTmpFormula(r,seq1+(seq-1)/2);
918  Biddy_Clean();
919  seq1--;
920 #endif
921 #endif
922  } else {
923  t = *(--LP1);
924  ZF_LOGI("P_AND");
925  tmp = Biddy_And(r,t);
926  *(++LP2) = tmp;
927 #ifdef USE_BIDDY
928 #ifdef USE_GARBAGE_COLLECTION
929  Biddy_AddTmpFormula(tmp,seq1+(seq-1)/2);
930  Biddy_Clean();
931  seq1--;
932 #endif
933 #endif
934 #ifdef USE_CUDD
935  Cudd_Ref(tmp);
936  Cudd_RecursiveDeref(manager,r);
937  Cudd_RecursiveDeref(manager,t);
938 #endif
939  }
940  }
941  fifo1 = fifo2;
942  fifo2 = LP1;
943  LP1 = LP2;
944 
945  /* TO BE CONSISTENT YOU HAVE TO REVERSE ORDERING OF ELEMENTS */
946  LP1++;
947  LP2 = fifo2;
948  LP2--;
949  while(LP1 != fifo1) {
950  *(++LP2) = *(--LP1);
951  }
952  fifo1 = fifo2;
953  fifo2 = LP1;
954  LP1 = LP2;
955 
956  } while (LP1 != fifo1);
957  r = *(LP1);
958 #endif
959 
960 /* POSTPONE And OPERATIONS USING LIFO */
961 #if defined(POSTPONE_LIFO) || defined(POSTPONE_REVERSE_LIFO)
962 #ifdef REPORT
963  printf("\nPOSTPONED And OPERATIONS USING LIFO\n");
964 #endif
965 #ifdef USE_CUDD
966  Cudd_RecursiveDeref(manager,r);
967 #endif
968  i = 0;
969  while(LP1 != fifo1) {
970  r = *(LP1--);
971  t = *(LP1--);
972  ZF_LOGI("P_AND");
973  tmp = Biddy_And(r,t);
974  *(++LP1) = tmp;
975 #ifdef USE_BIDDY
976 #ifdef USE_GARBAGE_COLLECTION
977  Biddy_AddTmpFormula(tmp,1);
978  Biddy_Clean();
979 #endif
980 #endif
981 #ifdef USE_CUDD
982  Cudd_Ref(tmp);
983  Cudd_RecursiveDeref(manager,r);
984  Cudd_RecursiveDeref(manager,t);
985 #endif
986  }
987  r = *(LP1);
988 #endif
989 
990  free(fifo1);
991  free(fifo2);
992 
993  /* EXPLICIT CALL TO GC TO MINIMIZE THE RESULT - IMPLEMENTED FOR BIDDY, ONLY */
994 #ifdef USE_BIDDY_X
995  Biddy_AutoGC();
996 #endif
997 
998  /* SIFTING TO MINIMIZE THE RESULT - IMPLEMENTED FOR BIDDY, ONLY */
999 #ifdef USE_BIDDY
1000 #ifdef NOT_POSTPONE
1001 #ifdef USE_SIFTING
1002  ZF_LOGI("F_SIFT");
1003  Biddy_Sifting(NULL,FALSE);
1004 #endif
1005 #ifdef USE_SIFTING_R
1006  ZF_LOGI("F_SIFT_R");
1007  Biddy_Sifting(r,FALSE);
1008 #endif
1009 #endif
1010 #endif
1011 
1012  ZF_LOGI("EXIT");
1013 
1014  /* PROFILING */
1015  /*
1016  checkOutOfLimits(size,elapsedtime);
1017  */
1018 
1019  elapsedtime = clock()-elapsedtime;
1020 
1021  /*
1022  if (clock_gettime(CLOCK_PROCESS_CPUTIME_ID,&stoptimex) == -1) printf("ERROR WITH clock_gettime!\n");
1023  fprintf(stderr,"clock_gettime() TIME = %.2f\n",(stoptimex.tv_sec-elapsedtimex.tv_sec)+(stoptimex.tv_nsec-elapsedtimex.tv_nsec)/1000000000.0);
1024  */
1025 
1026  /* RESULT */
1027 #ifdef REPORT
1028  printf("\n");
1030  printf("Resulting function r has %.0f minterms.\n",Biddy_CountMinterm(r,n));
1031  printf("Resulting function r depends on %u variables.\n",n);
1032  printf("BDD for resulting function r has %u nodes.\n",Biddy_NodeNumber(r));
1033  printf("BDD for the resulting function has density = %.2f.\n",Biddy_DensityBDD(r,0));
1034 #ifdef USE_BIDDY
1035  printf("Resulting function has density = %e.\n",Biddy_DensityFunction(r,0));
1036  printf("BDD without complemented edges for resulting function r has %u nodes (including both constants).\n",Biddy_NodeNumberPlain(r));
1037 #endif
1038 #endif
1039 
1040  /* CONVERT TO OBDD AND REPORT THE SIZE OF THE EQUIVALENT OBDD - Biddy ONLY! */
1041  /*
1042  {
1043  Biddy_Manager MNGOBDD;
1044  Biddy_Edge obdd;
1045  Biddy_InitMNG(&MNGOBDD,BIDDYTYPEOBDD);
1046  obdd = Biddy_Copy(MNGOBDD,r);
1047  n = Biddy_Managed_DependentVariableNumber(MNGOBDD,obdd);
1048  printf("Function represented by the equivalent OBDD depends on %u variables.\n",n);
1049  printf("Function represented by the equivalent OBDD has %.0f minterms.\n",Biddy_Managed_CountMinterm(MNGOBDD,obdd,n));
1050  printf("Function represented by the equivalent OBDD has density = %e.\n",Biddy_Managed_DensityFunction(MNGOBDD,obdd,0));
1051  printf("Equivalent OBDD has %u nodes.\n",Biddy_Managed_NodeNumber(MNGOBDD,obdd));
1052  printf("Equivalent OBDD without complemented edges for resulting function r has %u nodes (including both constants).\n",Biddy_Managed_NodeNumberPlain(MNGOBDD,obdd));
1053  printf("Equivalent OBDD has density = %.2f.\n",Biddy_Managed_DensityBDD(MNGOBDD,obdd,0));
1054  }
1055  */
1056 
1057  /* CONVERT TO ZBDD AND REPORT THE SIZE OF THE EQUIVALENT TZBDD - Biddy ONLY! */
1058  /*
1059  {
1060  Biddy_Manager MNGZBDD;
1061  Biddy_Edge zbdd;
1062  Biddy_InitMNG(&MNGZBDD,BIDDYTYPEZBDD);
1063  zbdd = Biddy_Copy(MNGZBDD,r);
1064  printf("ZBDD for function r has %u nodes.\n",Biddy_Managed_NodeNumber(MNGZBDD,zbdd));
1065  }
1066  */
1067 
1068  /* CONVERT TO TZBDD AND REPORT THE SIZE OF THE EQUIVALENT TZBDD - Biddy ONLY! */
1069  /*
1070  {
1071  Biddy_Manager MNGTZBDD;
1072  Biddy_Edge tzbdd;
1073  Biddy_InitMNG(&MNGTZBDD,BIDDYTYPETZBDD);
1074  tzbdd = Biddy_Copy(MNGTZBDD,r);
1075  printf("TZBDD for function r has %u nodes.\n",Biddy_Managed_NodeNumber(MNGTZBDD,tzbdd));
1076  }
1077  */
1078 
1079  /* DUMP RESULT USING GRAPHVIZ/DOT */
1080  /*
1081 #ifdef USE_BIDDY
1082  Biddy_WriteDot("8queens-biddy.dot",r,"r",-1,FALSE);
1083 #elif USE_CUDD
1084  {
1085  FILE * fp;
1086  fp = fopen("8queens-cudd.dot","w");
1087  Cudd_DumpDot(manager,1,&r,NULL,NULL,fp);
1088  fclose(fp);
1089  }
1090 #endif
1091  */
1092 
1093  /* We have problems with passing stdout in the case you compile this file */
1094  /* with MINGW and use biddy.dll generated with Visual Studio. */
1095  /* In such cases, please, use Biddy_PrintInfo(NULL) */
1096 #ifdef REPORT
1097  printf("\n");
1098  Biddy_PrintInfo(stdout);
1099 #endif
1100 
1101  /* SIFTING ON THE RESULT - THIS IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
1102  /*
1103 #ifdef USE_BIDDY
1104  Biddy_Sifting(NULL,FALSE);
1105 #endif
1106 #ifdef USE_CUDD
1107  Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT,0);
1108 #endif
1109 #ifdef REPORT
1110  n = Biddy_DependentVariableNumber(r);
1111  printf("(AFTER SIFTING) Resulting function r depends on %u variables.\n",n);
1112  printf("(AFTER SIFTING) Resulting function r has %.0f minterms.\n",Biddy_CountMinterm(r,n));
1113  printf("(AFTER SIFTING) BDD for resulting function r has %u nodes.\n",Biddy_NodeNumber(r));
1114 #endif
1115  */
1116 
1117 #ifndef REPORT
1118  /*
1119  if (Biddy_GetManagerType() == BIDDYTYPEOBDD) {
1120  fprintf(stderr,"(OBDD) ");
1121  }
1122  else if (Biddy_GetManagerType() == BIDDYTYPEZBDD) {
1123  fprintf(stderr,"(ZBDD) ");
1124  }
1125  else if (Biddy_GetManagerType() == BIDDYTYPETZBDD) {
1126  fprintf(stderr,"(TZBDD) ");
1127  }
1128  else {
1129  fprintf(stderr,"(unknown BDD type)");
1130  exit(1);
1131  }
1132  n = Biddy_DependentVariableNumber(r);
1133  fprintf(stderr,"Resulting function r has %.0f minterms.\n",Biddy_CountMinterm(r,n));
1134  */
1135 #endif
1136 
1137  /* REPORT ELAPSED TIME */
1138  /*
1139  fprintf(stderr,"clock() TIME = %.2f\n",elapsedtime/(1.0*CLOCKS_PER_SEC));
1140  */
1141 
1142 #ifdef REPORT
1143  printf("\nCALCULATION FINISHED\n");
1144 #endif
1145 
1146  /* PROFILING */
1147  /*
1148 #ifdef USE_BIDDY
1149  fprintf(stderr,"%2u, ",size);
1150 #ifdef MINGW
1151  fprintf(stderr,"%I64u, ",Biddy_ReadMemoryInUse());
1152 #else
1153  fprintf(stderr,"%10llu, ",Biddy_ReadMemoryInUse());
1154 #endif
1155  if (Biddy_NodeTableANDORRecursiveNumber()) {
1156  fprintf(stderr,"%llu, ",Biddy_NodeTableANDORRecursiveNumber());
1157  }
1158  fprintf(stderr,"%2u, ",Biddy_NodeTableGCNumber());
1159  if (Biddy_NodeTableGCObsoleteNumber()) {
1160  fprintf(stderr,"%llu, ",Biddy_NodeTableGCObsoleteNumber());
1161  fprintf(stderr,"%.2f, ",Biddy_NodeTableGCTime()/(1.0*CLOCKS_PER_SEC));
1162  }
1163  fprintf(stderr,"%.2f\n",elapsedtime/(1.0*CLOCKS_PER_SEC));
1164 #endif
1165 #ifdef USE_CUDD
1166  fprintf(stderr,"%u, ",size);
1167  fprintf(stderr,"%zu, ",Cudd_ReadMemoryInUse(manager));
1168  fprintf(stderr,"0, ");
1169  fprintf(stderr,"%.2f\n",elapsedtime/(1.0*CLOCKS_PER_SEC));
1170 #endif
1171  */
1172 
1173  /* PROFILING */
1174  /*
1175  printf("\n");
1176  Biddy_PrintInfo(stdout);
1177  */
1178 
1179  /* EXIT */
1180 #ifdef USE_BIDDY
1181  Biddy_Exit();
1182 #endif
1183 #ifdef USE_CUDD
1184  Cudd_RecursiveDeref(manager,r);
1185 #ifdef REPORT
1186  printf("CUDD: nodes with non-zero reference counts: %d\n",Cudd_CheckZeroRef(manager));
1187 #endif
1188  Cudd_Quit(manager);
1189 #endif
1190 
1191 }
#define Biddy_CountMinterm(f, nvars)
Definition: biddy.h:905
void * Biddy_Edge
Definition: biddy.h:221
#define Biddy_GetManagerType()
Definition: biddy.h:280
#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_DependentVariableNumber(f)
Definition: biddy.h:890
#define Biddy_NodeNumberPlain(f)
Definition: biddy.h:885
#define Biddy_GetConstantOne()
Definition: biddy.h:347
#define Biddy_PrintInfo(f)
Definition: biddy.h:927
#define Biddy_Or(f, g)
Definition: biddy.h:486
#define Biddy_DensityFunction(f, nvars)
Definition: biddy.h:912
#define Biddy_NodeNumber(f)
Definition: biddy.h:735
#define Biddy_Not(f)
Definition: biddy.h:467
#define Biddy_GetConstantZero()
Definition: biddy.h:340
#define Biddy_Exit()
Definition: biddy.h:272
File biddy.h contains declaration of all external data structures.
char Biddy_Boolean
Definition: biddy.h:191
#define Biddy_NodeTableSize()
Definition: biddy.h:755
#define Biddy_GetVariableEdge(v)
Definition: biddy.h:374
#define Biddy_ReadMemoryInUse()
Definition: biddy.h:922
#define Biddy_SetManagerParameters(gcr, gcrF, gcrX, rr, rrF, rrX, st, fst, cst, fcst)
Definition: biddy.h:285
#define Biddy_DensityBDD(f, nvars)
Definition: biddy.h:917
char * Biddy_String
Definition: biddy.h:194