Biddy  1.7.4
An academic Binary Decision Diagrams package
biddy-example-8queens.c
1 /* $Revision: 356 $ */
2 /* $Date: 2017-12-13 22:30:46 +0100 (sre, 13 dec 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 (remove -static if you have Biddy as a dynamic library): */
10 /* gcc -DNOREPORT -DNOPROFILE -DEVENTLOG_NONE -DBIDDY -DOBDD -DUNIX -O2 -o biddy-example-8queens-obdd biddy-example-8queens.c -I. -L./bin -static -lbiddy -lgmp */
11 /* gcc -DNOREPORT -DNOPROFILE -DEVENTLOG_NONE -DBIDDY -DOBDDC -DUNIX -O2 -o biddy-example-8queens-obddc biddy-example-8queens.c -I. -L./bin -static -lbiddy -lgmp */
12 /* gcc -DNOREPORT -DNOPROFILE -DEVENTLOG_NONE -DBIDDY -DZBDDC -DUNIX -O2 -o biddy-example-8queens-zbddc biddy-example-8queens.c -I. -L./bin -static -lbiddy -lgmp */
13 /* gcc -DNOREPORT -DNOPROFILE -DEVENTLOG_NONE -DBIDDY -DTZBDD -DUNIX -O2 -o biddy-example-8queens-tzbdd biddy-example-8queens.c -I. -L./bin -static -lbiddy -lgmp */
14 /* gcc -DNOREPORT -DEVENTLOG_NONE -DCUDD -DOBDDC -O2 -o cudd-example-8queens-obddc biddy-example-8queens.c -I ../cudd/include/ -L ../cudd/lib/ -lcudd -lm */
15 /* gcc -DNOREPORT -DEVENTLOG_NONE -DCUDD -DZBDDC -O2 -o cudd-example-8queens-zbddc biddy-example-8queens.c -I ../cudd/include/ -L ../cudd/lib/ -lcudd -lm */
16 
17 /* for stats with more details, use BIDDYEXTENDEDSTATS_YES in biddyInt.h and use -lm for linking */
18 
19 /* default size, this can be overriden via argument */
20 #define SIZE 9
21 #define USE_GARBAGE_COLLECTION
22 
23 /* for BIDDY there are 3 variants possible: */
24 /* NOT_USE_SIFTING, USE_SIFTING, USE_SIFTING_R */
25 #define NOT_USE_SIFTING
26 
27 /* there are 5 variants possible */
28 /* NOT_POSTPONE, POSTPONE_FIFO, POSTPONE_LIFO, POSTPONE_REVERSE_FIFO, POSTPONE_REVERSE_LIFO */
29 #define NOT_POSTPONE
30 
31 /* event log (EVENTLOG_TIME, EVENTLOG_SIZE, or EVENTLOG_RESULT) */
32 #ifdef EVENTLOG_TIME
33 # define ZF_LOGI(x) {static unsigned int zfstat = 0;printf(x);printf("#%u,%.2f\n",++zfstat,clock()/(1.0*CLOCKS_PER_SEC));}
34 #endif
35 #ifdef EVENTLOG_SIZE
36 # ifdef BIDDY
37 # define ZF_LOGI(x) {static unsigned int zfstat = 0;printf(x);printf("#%u,%u,%u\n",++zfstat,Biddy_NodeTableNum(),Biddy_NodeTableSize());}
38 # endif
39 # ifdef CUDD
40 # define ZF_LOGI(x) {static unsigned int zfstat = 0;printf(x);printf("#%u,%u,%u\n",++zfstat,Cudd_ReadKeys(manager),Cudd_ReadSlots(manager));}
41 # endif
42 #endif
43 #ifdef EVENTLOG_RESULT
44 # ifdef BIDDY
45 # define ZF_LOGI(x) {static unsigned int zfstat = 0;printf(x);printf("#%u,%u\n",++zfstat,Biddy_CountNodes(r));}
46 # endif
47 # ifdef CUDD
48 # define ZF_LOGI(x) {static unsigned int zfstat = 0;printf(x);printf("#%u,%u\n",++zfstat,Cudd_DagSize(r));}
49 # endif
50 #endif
51 #ifndef ZF_LOGI
52 # define ZF_LOGI(x)
53 #endif
54 
55 #include <stdio.h>
56 #include <string.h>
57 #include <ctype.h>
58 #include <time.h>
59 
60 #include "biddy-cudd.h"
61 
62 void checkOutOfLimits(unsigned int size, clock_t elapsedtime) {
63 #ifdef BIDDY
64  if ((size == 10) && (Biddy_NodeTableSize() > 4194304)) {
65  fprintf(stderr,"10, -1, -1, -1\n");
66  exit(0);
67  }
68  if ((size == 9) && (Biddy_ReadMemoryInUse() > 120000000)) {
69  fprintf(stderr,"9, -1, -1, -1\n");
70  exit(0);
71  }
72  if ((size == 10) && (Biddy_ReadMemoryInUse() > 350000000)) {
73  fprintf(stderr,"10, -1, -1, -1\n");
74  exit(0);
75  }
76 #endif
77 }
78 
79 int main(int argc, char** argv) {
80  unsigned int i,j,k,n,size,seq;
81  Biddy_Edge **board,**board_not;
82  Biddy_Edge tmp;
83  Biddy_Edge t,r;
84  Biddy_Edge *fifo1,*LP1;
85  Biddy_Edge *fifo2,*LP2;
86 #if defined(POSTPONE_FIFO) || defined(POSTPONE_REVERSE_FIFO)
87  unsigned int seq1;
88 #endif
89 
90  clock_t elapsedtime;
91 
92  if (argc > 1) {
93 #pragma warning(suppress: 6031)
94  sscanf(argv[1],"%u",&size);
95  } else {
96  size = SIZE;
97  }
98 
99  if ((size < 2) || (size > 15)) {
100  printf("WRONG SIZE!\n");
101  exit(0);
102  }
103 
104  setbuf(stdout, NULL);
105 
106 #ifdef PROFILE
107  printf("!!!");
108 #endif
109 
110  elapsedtime = clock();
111 
112 #include "biddy-cudd.c" /* this will initialize BDD manager */
113 
114  LP1 = fifo1 = (Biddy_Edge *) malloc((4 * size * size + size) * sizeof(Biddy_Edge));
115  LP2 = fifo2 = (Biddy_Edge *) malloc((4 * size * size + size) * sizeof(Biddy_Edge));
116  LP1--;
117 
118 #ifdef BIDDY
119  seq = 0;
120 #endif
121 
122  board = (Biddy_Edge **) malloc((size+1)*sizeof(Biddy_Edge *));
123  board_not = (Biddy_Edge **) malloc((size+1)*sizeof(Biddy_Edge *));
124  for (i=0; i<=size; i++) {
125  board[i] = (Biddy_Edge *) malloc((size+1)*sizeof(Biddy_Edge));
126  board_not[i] = (Biddy_Edge *) malloc((size+1)*sizeof(Biddy_Edge));
127  }
128 
129 #ifdef BIDDY
130  if ((argc == 1) || (argc == 2)) {
131  Biddy_SetManagerParameters(-1,-1,-1,-1,-1,-1,-1,-1);
132  }
133  else if (argc == 8) {
134  int gcr,gcrF,gcrX;
135  int rr,rrF,rrX;
136  sscanf(argv[2],"%d",&gcr);
137  sscanf(argv[3],"%d",&gcrF);
138  sscanf(argv[4],"%d",&gcrX);
139  sscanf(argv[5],"%d",&rr);
140  sscanf(argv[6],"%d",&rrF);
141  sscanf(argv[7],"%d",&rrX);
142  Biddy_SetManagerParameters(gcr/100.0,gcrF/100.0,gcrX/100.0,rr/100.0,rrF/100.0,rrX/100.0,-1,-1);
143  printf("%d, %d, %d, %d, %d, %d, ",gcr,gcrF,gcrX,rr,rrF,rrX);
144  }
145  else if (argc == 11) {
146  int gcr,gcrF,gcrX;
147  int rr,rrF,rrX;
148  int st,cst;
149  sscanf(argv[2],"%d",&gcr);
150  sscanf(argv[3],"%d",&gcrF);
151  sscanf(argv[4],"%d",&gcrX);
152  sscanf(argv[5],"%d",&rr);
153  sscanf(argv[6],"%d",&rrF);
154  sscanf(argv[7],"%d",&rrX);
155  sscanf(argv[8],"%d",&st);
156  sscanf(argv[9],"%d",&cst);
157  Biddy_SetManagerParameters(gcr/100.0,gcrF/100.0,gcrX/100.0,rr/100.0,rrF/100.0,rrX/100.0,st/100.0,cst/100.0);
158  printf("%d, %d, %d, %d, %d, %d, ",gcr,gcrF,gcrX,rr,rrF,rrX);
159  }
160  else {
161  printf("Wrong number of parameters!\n");
162  printf("USAGE (short): biddy-example-8queens SIZE GCR GCRF GCRX RR RRF RRX\n");
163  printf("USAGE (long): biddy-example-8queens SIZE GCR GCRF GCRX RR RRF RRX ST CST\n");
164  printf("All parameters should be integer numbers >= 0");
165  exit(0);
166  }
167 #endif
168 
169 #ifdef CUDD
170  Cudd_SetMaxCacheHard(manager,262144);
171 #endif
172 
173  for (i=1; i<=size; i++) {
174 #pragma warning(suppress: 6011)
175  board[0][i] = board[i][0] = NULL;
176  board_not[0][i] = board_not[i][0] = NULL;
177  }
178 
179  /* create BDD variables */
180  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC) ||
181  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC))
182  {
183  for (i=1; i<=size; i++) {
184  for (j=1; j<=size; j++) {
185  board[i][j] = Biddy_AddVariable();
186  REF(board[i][j]);
187  board_not[i][j] = Biddy_Not(board[i][j]);
188  REF(board_not[i][j]);
189  }
190  }
191  }
192 
193  /* for Biddy, ZBDD variables are added in the reverse order to get consistent results */
194 #ifdef BIDDY
195  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC))
196  {
197  for (i=1; i<=size; i++) {
198  for (j=1; j<=size; j++) {
199  board[size-i+1][size-j+1] = Biddy_AddVariable();
200  board_not[size-i+1][size-j+1] = Biddy_Not(board[size-i+1][size-j+1]);
201  }
202  }
203  }
204 #endif
205 #ifdef CUDD
206  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC))
207  {
208  for (i=1; i<=size; i++) {
209  for (j=1; j<=size; j++) {
210  board[i][j] = Biddy_AddVariable();
211  REF(board[i][j]);
212  board_not[i][j] = Biddy_Not(board[i][j]);
213  REF(board_not[i][j]);
214  }
215  }
216  }
217 #endif
218 
219  /* for ZBDDs, by adding new variables all the existing variables are changed */
220  /* after adding the last variable we have to refresh edges in board[i][j] and board_not[i][j] */
221  /* NOTE: for Biddy, ZBDD variables are added in the reverse order */
222  /* NOTE: for Biddy, user variables start with index 1 */
223  /* NOTE: for CUDD, user variables start with index 0 */
224  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC))
225  {
226 #ifdef BIDDY
227  /* user variables in Biddy start with index 1 */
228  for (i=1; i<=size; i++) {
229  for (j=1; j<=size; j++) {
230  board[i][j] = Biddy_GetVariableEdge(size*size-((i-1)*size+(j-1)));
231  board_not[i][j] = Biddy_Not(board[i][j]);
232  }
233  }
234 #endif
235 #ifdef CUDD
236  /* user variables in CUDD start with index 0 */
237  for (i=1; i<=size; i++) {
238  for (j=1; j<=size; j++) {
239  DEREF(board[i][j]);
240  board[i][j] = Cudd_zddIthVar(manager,(i-1)*size+(j-1));
241  REF(board[i][j]);
242  DEREF(board_not[i][j]);
243  board_not[i][j] = Biddy_Not(board[i][j]);
244  REF(board_not[i][j]);
245  }
246  }
247 #endif
248  }
249 
250  /* for TZBDDs, by adding new variables the negations of all the existing variables are changed */
251  /* after adding the last variable we have to refresh edges in board_not[i][j] */
252  /* NOTE: TZBDDs are supported only in Biddy */
253  if ((Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC))
254  {
255  for (i=1; i<=size; i++) {
256  for (j=1; j<=size; j++) {
257  board_not[i][j] = Biddy_Not(board[i][j]);
258  }
259  }
260  }
261 
262 /* For OBDDs, ZBDDs and TZBDDs, preserve board_not[i][j], because they are not a simple complemented edge */
263 /* TO DO: replace Biddy_AddPersistentFormula with the correct MARK_N */
264 #ifdef BIDDY
265 #ifdef NOT_POSTPONE
266  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) ||
267  (Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC) ||
268  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC))
269  {
270  for (i=1; i<=size; i++) {
271  for (j=1; j<=size; j++) {
272  Biddy_AddPersistentFormula(NULL,board_not[i][j]);
273  }
274  }
275  }
276 #endif
277 #endif
278 
279  r = Biddy_GetConstantOne();
280  REF(r);
281 
282  ZF_LOGI("INIT");
283 
284  /* ROWS */
285 #ifdef REPORT
286  printf("\nSTARTING ROWS\n");
287 #endif
288  for (i=1; i<=size; i++) {
289 #ifdef REPORT
290  printf("(%d/%d-%u)",i,size,Biddy_CountNodes(r));
291 #endif
292  for (j=1; j<=size; j++) {
293  t = Biddy_GetConstantOne();
294  REF(t);
295  for (k=1; k<=size; k++) {
296  if (k != j) {
297  ZF_LOGI("R_AND");
298  tmp = Biddy_And(t,board_not[i][k]);
299  REF(tmp);
300  DEREF(t);
301  t = tmp;
302  }
303  }
304  ZF_LOGI("R_OR");
305  tmp = Biddy_Or(t,board_not[i][j]);
306 #ifdef NOT_POSTPONE
307  MARK(r);
308  MARK(tmp);
309  SWEEP();
310 #endif
311  REF(tmp);
312  DEREF(t);
313  t = tmp;
314 
315 #ifdef NOT_POSTPONE
316  ZF_LOGI("R_AND");
317  tmp = Biddy_And(r,t);
318  MARK(tmp);
319  SWEEP();
320  REF(tmp);
321  DEREF(t);
322  DEREF(r);
323  r = tmp;
324 #else
325  *(++LP1) = t;
326 #endif
327 
328  ZF_LOGI("R_MEM");
329 
330 #ifdef POSTPONE_FIFO
331  seq++;
332  MARK_N(t,(seq-1)/2);
333 #endif
334 #ifdef POSTPONE_REVERSE_FIFO
335  seq++;
336  MARK_N(t,(4 * size * size + size - seq)/2);
337 #endif
338 #ifdef POSTPONE_LIFO
339  seq++;
340  if (seq == 1) {
341  MARK_N(t,seq-1);
342  } else {
343  MARK_N(t,seq-2);
344  }
345 #endif
346 #ifdef POSTPONE_REVERSE_LIFO
347  seq++;
348  MARK_N(t,(4 * size * size + size) - seq - 1);
349 #endif
350 
351  }
352  }
353 
354 #ifdef PROFILE
355  checkOutOfLimits(size,elapsedtime);
356 #endif
357 
358  /* SIFTING AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
359  /* IT IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
360 #ifdef BIDDY
361 #ifdef NOT_POSTPONE
362 #ifdef USE_SIFTING
363  ZF_LOGI("R_SIFT");
364  Biddy_Sifting(NULL,FALSE);
365 #endif
366 #ifdef USE_SIFTING_R
367  ZF_LOGI("R_SIFT_R");
368  Biddy_Sifting(r,FALSE);
369 #endif
370 #endif
371 #endif
372 
373  /* COLUMNS */
374 #ifdef REPORT
375  printf("\nSTARTING COLUMNS\n");
376 #endif
377  for (i=1; i<=size; i++) {
378 #ifdef REPORT
379  printf("(%d/%d-%u)",i,size,Biddy_CountNodes(r));
380 #endif
381  for (j=1; j<=size; j++) {
382  t = Biddy_GetConstantOne();
383  REF(t);
384  for (k=1; k<=size; k++) {
385  if (k != i) {
386  ZF_LOGI("C_AND");
387  tmp = Biddy_And(t,board_not[k][j]);
388  REF(tmp);
389  DEREF(t);
390  t = tmp;
391  }
392  }
393  ZF_LOGI("C_OR");
394  tmp = Biddy_Or(t,board_not[i][j]);
395 #ifdef NOT_POSTPONE
396  MARK(r);
397  MARK(tmp);
398  SWEEP();
399 #endif
400  REF(tmp);
401  DEREF(t);
402  t = tmp;
403 
404 #ifdef NOT_POSTPONE
405  ZF_LOGI("C_AND");
406  tmp = Biddy_And(r,t);
407  MARK(tmp);
408  SWEEP();
409  REF(tmp);
410  DEREF(t);
411  DEREF(r);
412  r = tmp;
413 #else
414  *(++LP1) = t;
415 #endif
416 
417  ZF_LOGI("C_MEM");
418 
419 #ifdef POSTPONE_FIFO
420  seq++;
421  MARK_N(t,(seq-1)/2);
422 #endif
423 #ifdef POSTPONE_REVERSE_FIFO
424  seq++;
425  MARK_N(t,(4 * size * size + size - seq)/2);
426 #endif
427 #ifdef POSTPONE_LIFO
428  seq++;
429  MARK_N(t,seq-2);
430 #endif
431 #ifdef POSTPONE_REVERSE_LIFO
432  seq++;
433  MARK_N(t,(4 * size * size + size) - seq - 1);
434 #endif
435 
436  }
437  }
438 
439 #ifdef PROFILE
440  checkOutOfLimits(size,elapsedtime);
441 #endif
442 
443  /* SIFTING AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
444  /* IT IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
445 #ifdef BIDDY
446 #ifdef NOT_POSTPONE
447 #ifdef USE_SIFTING
448  ZF_LOGI("C_SIFT");
449  Biddy_Sifting(NULL,FALSE);
450 #endif
451 #ifdef USE_SIFTING_R
452  ZF_LOGI("C_SIFT_R");
453  Biddy_Sifting(r,FALSE);
454 #endif
455 #endif
456 #endif
457 
458  /* RISING DIAGONALS */
459 #ifdef REPORT
460  printf("\nSTARTING RISING DIAGONALS\n");
461 #endif
462  for (i=1; i<=size; i++) {
463 #ifdef REPORT
464  printf("(%d/%d-%u)",i,size,Biddy_CountNodes(r));
465 #endif
466  for (j=1; j<=size; j++) {
467  t = Biddy_GetConstantOne();
468  REF(t);
469  for (k=1; k<=size; k++) {
470  if ((j+k-i >= 1) && (j+k-i <= size) && (k != i)) {
471  ZF_LOGI("RD_AND");
472  tmp = Biddy_And(t,board_not[k][j+k-i]);
473  REF(tmp);
474  DEREF(t);
475  t = tmp;
476  }
477  }
478  ZF_LOGI("RD_OR");
479  tmp = Biddy_Or(t,board_not[i][j]);
480 #ifdef NOT_POSTPONE
481  MARK(r);
482  MARK(tmp);
483  SWEEP();
484 #endif
485  REF(tmp);
486  DEREF(t);
487  t = tmp;
488 
489 #ifdef NOT_POSTPONE
490  ZF_LOGI("RD_AND");
491  tmp = Biddy_And(r,t);
492  MARK(tmp);
493  SWEEP();
494  REF(tmp);
495  DEREF(t);
496  DEREF(r);
497  r = tmp;
498 #else
499  *(++LP1) = t;
500 #endif
501 
502  ZF_LOGI("RD_MEM");
503 
504 #ifdef POSTPONE_FIFO
505  seq++;
506  MARK_N(t,(seq-1)/2);
507 #endif
508 #ifdef POSTPONE_REVERSE_FIFO
509  seq++;
510  MARK_N(t,(4 * size * size + size - seq)/2);
511 #endif
512 #ifdef POSTPONE_LIFO
513  seq++;
514  MARK_N(t,seq-2);
515 #endif
516 #ifdef POSTPONE_REVERSE_LIFO
517  seq++;
518  MARK_N(t,(4 * size * size + size) - seq - 1);
519 #endif
520 
521  }
522  }
523 
524 #ifdef PROFILE
525  checkOutOfLimits(size,elapsedtime);
526 #endif
527 
528  /* SIFTING AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
529  /* IT IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
530 #ifdef BIDDY
531 #ifdef NOT_POSTPONE
532 #ifdef USE_SIFTING
533  ZF_LOGI("RD_SIFT");
534  Biddy_Sifting(NULL,FALSE);
535 #endif
536 #ifdef USE_SIFTING_R
537  ZF_LOGI("RD_SIFT_R");
538  Biddy_Sifting(r,FALSE);
539 #endif
540 #endif
541 #endif
542 
543  /* FALLING DIAGONALS */
544 #ifdef REPORT
545  printf("\nSTARTING FALLING DIAGONALS\n");
546 #endif
547  for (i=1; i<=size; i++) {
548 #ifdef REPORT
549  printf("(%d/%d-%u)",i,size,Biddy_CountNodes(r));
550 #endif
551  for (j=1; j<=size; j++) {
552  t = Biddy_GetConstantOne();
553  REF(t);
554  for (k=1; k<=size; k++) {
555  if ((j+i-k >= 1) && (j+i-k <= size) && (k != i)) {
556  ZF_LOGI("FD_AND");
557  tmp = Biddy_And(t,board_not[k][j+i-k]);
558  REF(tmp);
559  DEREF(t);
560  t = tmp;
561  }
562  }
563  ZF_LOGI("FD_OR");
564 #pragma warning(suppress: 6011)
565  tmp = Biddy_Or(t,board_not[i][j]);
566 #ifdef NOT_POSTPONE
567  MARK(r);
568  MARK(tmp);
569  SWEEP();
570 #endif
571  REF(tmp);
572  DEREF(t);
573  t = tmp;
574 
575 #ifdef NOT_POSTPONE
576  ZF_LOGI("FD_AND");
577  tmp = Biddy_And(r,t);
578  MARK(tmp);
579  SWEEP();
580  REF(tmp);
581  DEREF(t);
582  DEREF(r);
583  r = tmp;
584 #else
585  *(++LP1) = t;
586 #endif
587 
588  ZF_LOGI("FD_MEM");
589 
590 #ifdef POSTPONE_FIFO
591  seq++;
592  MARK_N(t,(seq-1)/2);
593 #endif
594 #ifdef POSTPONE_REVERSE_FIFO
595  seq++;
596  MARK_N(t,(4 * size * size + size - seq)/2);
597 #endif
598 #ifdef POSTPONE_LIFO
599  seq++;
600  MARK_N(t,seq-2);
601 #endif
602 #ifdef POSTPONE_REVERSE_LIFO
603  seq++;
604  MARK_N(t,(4 * size * size + size) - seq - 1);
605 #endif
606 
607  }
608  }
609 
610 #ifdef PROFILE
611  checkOutOfLimits(size,elapsedtime);
612 #endif
613 
614  /* SIFTING AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
615  /* IT IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
616 #ifdef BIDDY
617 #ifdef NOT_POSTPONE
618 #ifdef USE_SIFTING
619  ZF_LOGI("FD_SIFT");
620  Biddy_Sifting(NULL,FALSE);
621 #endif
622 #ifdef USE_SIFTING_R
623  ZF_LOGI("FD_SIFT_R");
624  Biddy_Sifting(r,FALSE);
625 #endif
626 #endif
627 #endif
628 
629  /* THERE MUST BE A QUEEN IN EACH ROW */
630 #ifdef REPORT
631  printf("\nSTARTING FINAL CALCULATONS\n");
632 #endif
633  for (i=1; i<=size; i++) {
634 #ifdef REPORT
635  printf("(%d/%d-%u)",i,size,Biddy_CountNodes(r));
636 #endif
637  t = Biddy_GetConstantZero();
638  REF(t);
639  for (j=1; j<=size; j++) {
640  ZF_LOGI("F_OR");
641  tmp = Biddy_Or(t,board[i][j]);
642  REF(tmp);
643  DEREF(t);
644  t = tmp;
645  }
646 
647 #ifdef NOT_POSTPONE
648  ZF_LOGI("F_AND");
649  tmp = Biddy_And(r,t);
650  MARK(tmp);
651  SWEEP();
652  REF(tmp);
653  DEREF(t);
654  DEREF(r);
655  r = tmp;
656 #else
657  *(++LP1) = t;
658 #endif
659 
660  ZF_LOGI("F_MEM");
661 
662 #ifdef POSTPONE_FIFO
663  seq++;
664  MARK_N(t,(seq-1)/2);
665 #endif
666 #ifdef POSTPONE_REVERSE_FIFO
667  seq++;
668  MARK_N(t,(4 * size * size + size - seq)/2);
669 #endif
670 #ifdef POSTPONE_LIFO
671  seq++;
672  MARK_N(t,seq-2);
673 #endif
674 #ifdef POSTPONE_REVERSE_LIFO
675  seq++;
676  if (seq == (4 * size *size + size)) {
677  MARK_N(t,4 * size * size + size - seq);
678  } else {
679  MARK_N(t,4 * size * size + size - seq - 1);
680  }
681 #endif
682 
683 #ifdef PROFILE
684  checkOutOfLimits(size,elapsedtime);
685 #endif
686 
687  }
688 
689 #ifdef PROFILE
690  checkOutOfLimits(size,elapsedtime);
691 #endif
692 
693  /* SIFTING AFTER EACH MAJOR PART - IMPLEMENTED FOR BIDDY, ONLY */
694  /* IT IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
695 #ifdef BIDDY
696 #ifdef NOT_POSTPONE
697 #ifdef USE_SIFTING
698  ZF_LOGI("FD_SIFT");
699  Biddy_Sifting(NULL,FALSE);
700 #endif
701 #ifdef USE_SIFTING_R
702  ZF_LOGI("FD_SIFT_R");
703  Biddy_Sifting(r,FALSE);
704 #endif
705 #endif
706 #endif
707 
708  ZF_LOGI("P_MEM");
709 
710 /* POSTPONED ELEMENTS WILL BE CALCULATED IN REVERSED ORDER */
711 #if defined(POSTPONE_FIFO) || defined(POSTPONE_LIFO)
712  LP1++;
713  LP2 = fifo2;
714  LP2--;
715  while(LP1 != fifo1) {
716  *(++LP2) = *(--LP1);
717  }
718  fifo1 = fifo2;
719  fifo2 = LP1;
720  LP1 = LP2;
721 #endif
722 
723 #ifdef NOT_POSTPONE
724 #ifdef REPORT
725  printf("\nAnd OPERATIONS ARE NOT POSTPONED\n");
726 #endif
727 #endif
728 
729 /* POSTPONE And OPERATIONS USING FIFO */
730 #if defined(POSTPONE_FIFO) || defined(POSTPONE_REVERSE_FIFO)
731 #ifdef REPORT
732  printf("\nPOSTPONED And OPERATIONS USING FIFO\n");
733 #endif
734  DEREF(r);
735  i = 0;
736  do {
737  LP1++;
738  LP2 = fifo2;
739  LP2--;
740  seq1 = (seq+1)/2;
741  seq = 0;
742  while(LP1 != fifo1) {
743  ZF_LOGI("P_MEM");
744  seq++;
745  r = *(--LP1);
746  if (LP1 == fifo1) {
747  *(++LP2) = r;
748  MARK_N(r,seq1+(seq-1)/2);
749  SWEEP();
750  seq1--;
751  } else {
752  t = *(--LP1);
753  ZF_LOGI("P_AND");
754  tmp = Biddy_And(r,t);
755  *(++LP2) = tmp;
756  MARK_N(tmp,seq1+(seq-1)/2);
757  SWEEP();
758  seq1--;
759  REF(tmp);
760  DEREF(manager,r);
761  DEREF(manager,t);
762  }
763  }
764  fifo1 = fifo2;
765  fifo2 = LP1;
766  LP1 = LP2;
767 
768  /* TO BE CONSISTENT YOU HAVE TO REVERSE ORDERING OF ELEMENTS */
769  LP1++;
770  LP2 = fifo2;
771  LP2--;
772  while(LP1 != fifo1) {
773  *(++LP2) = *(--LP1);
774  }
775  fifo1 = fifo2;
776  fifo2 = LP1;
777  LP1 = LP2;
778 
779  } while (LP1 != fifo1);
780  r = *(LP1);
781 #endif
782 
783 /* POSTPONE And OPERATIONS USING LIFO */
784 #if defined(POSTPONE_LIFO) || defined(POSTPONE_REVERSE_LIFO)
785 #ifdef REPORT
786  printf("\nPOSTPONED And OPERATIONS USING LIFO\n");
787 #endif
788  DEREF(r);
789  i = 0;
790  while(LP1 != fifo1) {
791  r = *(LP1--);
792  t = *(LP1--);
793  ZF_LOGI("P_AND");
794  tmp = Biddy_And(r,t);
795  *(++LP1) = tmp;
796  MARK(tmp);
797  SWEEP();
798  REF(tmp);
799  DEREF(r);
800  DEREF(t);
801  }
802  r = *(LP1);
803 #endif
804 
805  free(fifo1);
806  free(fifo2);
807 
808  /* SIFTING TO MINIMIZE THE RESULT - IMPLEMENTED FOR BIDDY, ONLY */
809 #ifdef BIDDY
810 #ifdef NOT_POSTPONE
811 #ifdef USE_SIFTING
812  ZF_LOGI("F_SIFT");
813  Biddy_Sifting(NULL,FALSE);
814 #endif
815 #ifdef USE_SIFTING_R
816  ZF_LOGI("F_SIFT_R");
817  Biddy_Sifting(r,FALSE);
818 #endif
819 #endif
820 #endif
821 
822  ZF_LOGI("EXIT");
823 
824 #ifdef PROFILE
825  checkOutOfLimits(size,elapsedtime);
826 #endif
827 
828  elapsedtime = clock()-elapsedtime;
829 
830  /* RESULT */
831 #ifdef REPORT
832  printf("\n");
834  printf("Resulting function r has %.0f minterms.\n",Biddy_CountMinterms(r,n));
835  printf("Resulting function r depends on %u variables.\n",n);
836  printf("BDD for resulting function r has %u nodes.\n",Biddy_CountNodes(r));
837  printf("BDD for the resulting function has density = %.2f.\n",Biddy_DensityOfBDD(r,0));
838 #ifdef BIDDY
839  printf("Resulting function has density = %e.\n",Biddy_DensityOfFunction(r,0));
840  printf("BDD without complemented edges for resulting function r has %u nodes (including both terminals).\n",Biddy_CountNodesPlain(r));
841 #endif
842 #else
844  printf("%.0f minterms, %u nodes\n",Biddy_CountMinterms(r,n),Biddy_CountNodes(r));
845 #endif
846 
847  /* CONVERT TO OBDD AND REPORT THE SIZE OF THE EQUIVALENT OBDD - Biddy ONLY! */
848  /*
849  {
850  Biddy_Manager MNGOBDD;
851  Biddy_Edge obdd;
852  Biddy_InitMNG(&MNGOBDD,BIDDYTYPEOBDDC);
853  obdd = Biddy_Copy(MNGOBDD,r);
854  n = Biddy_Managed_DependentVariableNumber(MNGOBDD,obdd);
855  printf("Function represented by the equivalent OBDD depends on %u variables.\n",n);
856  printf("Function represented by the equivalent OBDD has %.0f minterms.\n",Biddy_Managed_CountMinterms(MNGOBDD,obdd,n));
857  printf("Function represented by the equivalent OBDD has density = %e.\n",Biddy_Managed_DensityOfFunction(MNGOBDD,obdd,0));
858  printf("Equivalent OBDD has %u nodes.\n",Biddy_Managed_CountNodes(MNGOBDD,obdd));
859  printf("Equivalent OBDD without complemented edges for resulting function r has %u nodes (including both terminals).\n",Biddy_Managed_CountNodesPlain(MNGOBDD,obdd));
860  printf("Equivalent OBDD has density = %.2f.\n",Biddy_Managed_DensityOfBDD(MNGOBDD,obdd,0));
861  }
862  */
863 
864  /* CONVERT TO ZBDD AND REPORT THE SIZE OF THE EQUIVALENT TZBDD - Biddy ONLY! */
865  /*
866  {
867  Biddy_Manager MNGZBDD;
868  Biddy_Edge zbdd;
869  Biddy_InitMNG(&MNGZBDD,BIDDYTYPEZBDDC);
870  zbdd = Biddy_Copy(MNGZBDD,r);
871  printf("ZBDD for function r has %u nodes.\n",Biddy_Managed_CountNodes(MNGZBDD,zbdd));
872  }
873  */
874 
875  /* CONVERT TO TZBDD AND REPORT THE SIZE OF THE EQUIVALENT TZBDD - Biddy ONLY! */
876  /*
877  {
878  Biddy_Manager MNGTZBDD;
879  Biddy_Edge tzbdd;
880  Biddy_InitMNG(&MNGTZBDD,BIDDYTYPETZBDD);
881  tzbdd = Biddy_Copy(MNGTZBDD,r);
882  printf("TZBDD for function r has %u nodes.\n",Biddy_Managed_CountNodes(MNGTZBDD,tzbdd));
883  }
884  */
885 
886  /* DUMP RESULT USING GRAPHVIZ/DOT */
887  /*
888 #ifdef BIDDY
889  Biddy_WriteDot("8queens-biddy.dot",r,"r",-1,FALSE);
890 #elif CUDD
891  {
892  FILE * fp;
893  fp = fopen("8queens-cudd.dot","w");
894  Cudd_DumpDot(manager,1,&r,NULL,NULL,fp);
895  fclose(fp);
896  }
897 #endif
898  */
899 
900  /* We have problems with passing stdout in the case you compile this file */
901  /* with MINGW and use biddy.dll generated with Visual Studio. */
902  /* In such cases, please, use Biddy_PrintInfo(NULL) */
903 #ifdef REPORT
904  printf("\n");
905  Biddy_PrintInfo(stdout);
906 #endif
907 
908  /* SIFTING ON THE RESULT - THIS IS NOT VERY EFFECTIVE FOR THIS PROBLEM */
909  /*
910 #ifdef BIDDY
911  Biddy_Sifting(NULL,FALSE);
912 #endif
913 #ifdef CUDD
914  Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT,0);
915 #endif
916 #ifdef REPORT
917  n = Biddy_DependentVariableNumber(r);
918  printf("(AFTER SIFTING) Resulting function r depends on %u variables.\n",n);
919  printf("(AFTER SIFTING) Resulting function r has %.0f minterms.\n",Biddy_CountMinterms(r,n));
920  printf("(AFTER SIFTING) BDD for resulting function r has %u nodes.\n",Biddy_CountNodes(r));
921 #endif
922  */
923 
924 #ifndef REPORT
925  /*
926  if (Biddy_GetManagerType() == BIDDYTYPEOBDD) {
927  fprintf(stderr,"(OBDD) ");
928  }
929  else if (Biddy_GetManagerType() == BIDDYTYPEOBDDC) {
930  fprintf(stderr,"(OBDDC) ");
931  }
932  else if (Biddy_GetManagerType() == BIDDYTYPEZBDDC) {
933  fprintf(stderr,"(ZBDDC) ");
934  }
935  else if (Biddy_GetManagerType() == BIDDYTYPETZBDD) {
936  fprintf(stderr,"(TZBDD) ");
937  }
938  else {
939  fprintf(stderr,"(unknown BDD type)");
940  exit(0);
941  }
942  n = Biddy_DependentVariableNumber(r);
943  fprintf(stderr,"Resulting function r has %.0f minterms.\n",Biddy_CountMinterms(r,n));
944  */
945 #endif
946 
947  /* REPORT ELAPSED TIME */
948  /*
949  fprintf(stderr,"clock() TIME = %.2f\n",elapsedtime/(1.0*CLOCKS_PER_SEC));
950  */
951 
952 #ifdef REPORT
953  printf("\nCALCULATION FINISHED\n");
954 #endif
955 
956  /* PROFILING */
957  /**/
958 #ifdef BIDDY
959  fprintf(stderr,"#%u, ",size);
960 #ifdef MINGW
961  fprintf(stderr,"%I64u, ",Biddy_ReadMemoryInUse());
962 #else
963  fprintf(stderr,"%llu, ",Biddy_ReadMemoryInUse());
964 #endif
965 /*
966  if (Biddy_NodeTableFoaNumber()) {
967  fprintf(stderr,"%llu, ",Biddy_NodeTableFoaNumber());
968  }
969  if (Biddy_NodeTableFindNumber()) {
970  fprintf(stderr,"%llu, ",Biddy_NodeTableFindNumber());
971  }
972  if (Biddy_NodeTableCompareNumber()) {
973  fprintf(stderr,"%llu, ",Biddy_NodeTableCompareNumber());
974  }
975  if (Biddy_NodeTableAddNumber()) {
976  fprintf(stderr,"%llu, ",Biddy_NodeTableAddNumber());
977  }
978 */
979  fprintf(stderr,"%u, ",Biddy_NodeTableGCNumber());
981  fprintf(stderr,"%llu, ",Biddy_NodeTableGCObsoleteNumber());
982  }
984  fprintf(stderr,"%llu, ",Biddy_NodeTableANDORRecursiveNumber());
985  }
986  fprintf(stderr,"%.2f, ",Biddy_NodeTableGCTime()/(1.0*CLOCKS_PER_SEC));
987  fprintf(stderr,"%.2f",elapsedtime/(1.0*CLOCKS_PER_SEC));
988  fprintf(stderr,",\n");
989 #endif
990 #ifdef CUDD
991  fprintf(stderr,"%u, ",size);
992  fprintf(stderr,"%zu, ",Cudd_ReadMemoryInUse(manager));
993  fprintf(stderr,"0, ");
994  fprintf(stderr,"%.2f\n",elapsedtime/(1.0*CLOCKS_PER_SEC));
995 #endif
996  /**/
997 
998  /* PROFILING */
999  /*
1000  printf("\n");
1001  Biddy_PrintInfo(stdout);
1002  */
1003 
1004  /* EXIT */
1005  for (i=1; i<=size; i++) {
1006  for (j=1; j<=size; j++) {
1007  DEREF(board[i][j]);
1008  DEREF(board_not[i][j]);
1009  }
1010  }
1011  DEREF(r);
1012  free(board);
1013  free(board_not);
1014 
1015 #ifdef REPORT
1016 #ifdef CUDD
1017  printf("CUDD: nodes with non-zero reference counts: %d\n",Cudd_CheckZeroRef(manager));
1018 #endif
1019 #endif
1020 
1021  Biddy_Exit();
1022 }
#define Biddy_NodeTableGCNumber()
Definition: biddy.h:949
void * Biddy_Edge
Definition: biddy.h:262
#define Biddy_GetManagerType()
Definition: biddy.h:321
#define Biddy_And(f, g)
Definition: biddy.h:705
#define Biddy_Sifting(f, c)
Definition: biddy.h:651
#define Biddy_DependentVariableNumber(f)
Definition: biddy.h:1054
#define Biddy_GetConstantOne()
Definition: biddy.h:393
#define Biddy_PrintInfo(f)
Definition: biddy.h:1091
#define Biddy_Or(f, g)
Definition: biddy.h:713
#define Biddy_NodeTableGCTime()
Definition: biddy.h:954
#define Biddy_DensityOfBDD(f, nvars)
Definition: biddy.h:1081
#define Biddy_Not(f)
Definition: biddy.h:694
#define Biddy_GetConstantZero()
Definition: biddy.h:386
#define Biddy_CountMinterms(f, nvars)
Definition: biddy.h:1069
#define Biddy_NodeTableGCObsoleteNumber()
Definition: biddy.h:959
#define Biddy_Exit()
Definition: biddy.h:313
#define Biddy_CountNodesPlain(f)
Definition: biddy.h:1049
#define Biddy_NodeTableSize()
Definition: biddy.h:894
#define Biddy_DensityOfFunction(f, nvars)
Definition: biddy.h:1076
#define Biddy_GetVariableEdge(v)
Definition: biddy.h:430
#define Biddy_SetManagerParameters(gcr, gcrF, gcrX, rr, rrF, rrX, st, cst)
Definition: biddy.h:331
#define Biddy_ReadMemoryInUse()
Definition: biddy.h:1086
#define Biddy_CountNodes(f)
Definition: biddy.h:874
#define Biddy_NodeTableANDORRecursiveNumber()
Definition: biddy.h:994