Biddy  1.7.3
An academic Binary Decision Diagrams package
biddy-example-hanoi.c
1 /* $Revision: 309 $ */
2 /* $Date: 2017-09-21 08:18:54 +0200 (čet, 21 sep 2017) $ */
3 /* This file (biddy-example-hanoi.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 BASED ON WORK PUBLISHED ON CMU, 2005 */
8 /* Course name: Introduction to Model Checking */
9 /* Prof. Edmund Clarke */
10 /* http://www.cs.cmu.edu/~emc/15817-s05/ */
11 
12 /* The code using CUDD package is original */
13 /* The code using Biddy package was added by Robert Meolic */
14 
15 /* This example is compatible with Biddy v1.7 and CUDD v3.0.0 */
16 
17 /* COMPILE WITH: */
18 /* gcc -DREPORT -DUNIX -DUSE_BIDDY -DUSE_OBDDC -O2 -o biddy-example-hanoi-obdd biddy-example-hanoi.c -I. -L./bin -lbiddy -lgmp */
19 /* gcc -DREPORT -DUNIX -DUSE_BIDDY -DUSE_ZBDDC -O2 -o biddy-example-hanoi-zbdd biddy-example-hanoi.c -I. -L./bin -lbiddy -lgmp */
20 /* gcc -DREPORT -DUNIX -DUSE_BIDDY -DUSE_TZBDD -O2 -o biddy-example-hanoi-tzbdd biddy-example-hanoi.c -I. -L./bin -lbiddy -lgmp */
21 /* gcc -DREPORT -DUSE_CUDD -DUSE_OBDDC -O2 -o cudd-example-hanoi-obdd biddy-example-hanoi.c -I ../cudd/include/ -L ../cudd/lib/ -lcudd -lm */
22 /* gcc -DREPORT -DUSE_CUDD -DUSE_ZBDDC -O2 -o cudd-example-hanoi-zbdd biddy-example-hanoi.c -I ../cudd/include/ -L ../cudd/lib/ -lcudd -lm */
23 
24 /* Here are original comments */
25 /*
26 This example essentially illustrates reachability computation, which
27 is one of the core operations inside a model checker. In model
28 checking, the goal state represents the error state, and the model
29 checker either:
30 1. Discovers that the error state is unreachable if the fixed point is
31  achieved before hitting the error.
32 2. Discovers that the error is reachable. In that case it returns a
33  counterexample, which is a sequence of steps from the initial state
34  to the error state.
35 The above implementation does not produce a counterexample.
36 Exercise: Add counterexample generation to the above.
37 How:
38 You will need to store pointers to all the image BDDs. Starting from
39 the error state, compute a "reverse image", intersect with the
40 correspoding forward image, pick a state from the intersection and
41 repeat till you hit the initial state.
42 */
43 
44 /* Towers of Hanoi problem using BDDs */
45 /* number of towers = 3 */
46 /* number of disks = SIZE */
47 #define MAXSIZE 16
48 #define SIZE 10
49 
50 #ifdef USE_BIDDY
51 # include "biddy.h"
52 # define BDDNULL NULL
53 /* #define Biddy_Inv(f) Biddy_NOT(f) */ /* for compatibility with Biddy v1.6 */
54 #endif
55 
56 #ifdef USE_CUDD
57 # include <stdio.h>
58 # include <stdlib.h>
59 # include <stdint.h>
60 # include <string.h>
61 # include <ctype.h>
62 # include <stdarg.h>
63 # include <math.h>
64 # include "cudd.h"
65 # define BDDNULL NULL
66 # ifndef TRUE
67 # define TRUE (0 == 0)
68 # endif
69 # ifndef FALSE
70 # define FALSE !TRUE
71 # endif
72 typedef char *Biddy_String;
73 typedef char Biddy_Boolean;
74 typedef DdNode *Biddy_Edge;
75 DdManager * manager; /* BDD Manager */
76 #endif
77 
78 #include <time.h>
79 
80 #ifdef USE_CUDD
81 #ifndef USE_ZBDDC
82 #ifndef USE_OBDDC
83 #define USE_OBDDC
84 #endif
85 #endif
86 #define BIDDYTYPEOBDD 1
87 #define BIDDYTYPEOBDDC 2
88 #define BIDDYTYPEZBDD 3
89 #define BIDDYTYPEZBDDC 4
90 #define BIDDYTYPETZBDD 5
91 #define BIDDYTYPETZBDDC 6
92 #ifdef USE_OBDDC
93 #define Biddy_GetManagerType() BIDDYTYPEOBDDC
94 #define Biddy_GetConstantZero() Cudd_ReadLogicZero(manager)
95 #define Biddy_GetConstantOne() Cudd_ReadOne(manager)
96 #define Biddy_AddVariable() Cudd_bddNewVar(manager)
97 #define Biddy_Not(f) Cudd_Not(f)
98 #define Biddy_And(f,g) Cudd_bddAnd(manager,f,g)
99 #define Biddy_Or(f,g) Cudd_bddOr(manager,f,g)
100 #define Biddy_Xor(f,g) Cudd_bddXor(manager,f,g)
101 #define Biddy_Xnor(f,g) Cudd_bddXnor(manager,f,g)
102 #define Biddy_Compose(f,g,v) Cudd_bddCompose(manager,f,g,v-1)
103 #define Biddy_AndAbstract(f,g,c) Cudd_bddAndAbstract(manager,f,g,c)
104 #define Biddy_DependentVariableNumber(f) Cudd_SupportSize(manager,f)
105 #define Biddy_CountMinterm(f,n) Cudd_CountMinterm(manager,f,n)
106 #elif USE_ZBDDC
107 #define Biddy_GetManagerType() BIDDYTYPEZBDDC
108 #define Biddy_GetConstantZero() Cudd_ReadZero(manager)
109 #define Biddy_GetConstantOne() Cudd_ReadZddOne(manager,0)
110 #define Biddy_AddVariable() Cudd_zddIthVar(manager,Cudd_ReadZddSize(manager))
111 #define Biddy_Not(f) Cudd_zddDiff(manager,Cudd_ReadZddOne(manager,0),f)
112 #define Biddy_And(f,g) Cudd_zddIntersect(manager,f,g)
113 #define Biddy_Or(f,g) Cudd_zddUnion(manager,f,g)
114 #define Biddy_Xor(f,g) Cudd_
115 #define Biddy_Xnor(f,g) Cudd_
116 #define Biddy_Compose(f,g,v) Cudd_
117 #define Biddy_AndAbstract(f,g,c) Cudd_
118 #define Biddy_DependentVariableNumber(f) Cudd_ReadZddSize(manager) /* this is not always valid but there is no better option */
119 #define Biddy_CountMinterm(f,n) Cudd_zddCountMinterm(manager,f,n)
120 #endif
121 #define Biddy_ChangeVariableName(v,name) 0
122 #define Biddy_NodeNumber(f) Cudd_DagSize(f)
123 #define Biddy_DensityBDD(f,n) Cudd_Density(manager,f,n)
124 #define Biddy_NodeTableNum() Cudd_ReadKeys(manager)
125 #define Biddy_NodeTableSize() Cudd_ReadSlots(manager)
126 #define Biddy_ReadMemoryInUse() Cudd_ReadMemoryInUse(manager)
127 #define Biddy_PrintInfo(s) Cudd_PrintInfo(manager,s)
128 #endif
129 
130 Biddy_Edge v1[MAXSIZE][3]; /* the current state */
131 Biddy_Edge v2[MAXSIZE][3]; /* the next state */
132 
133 /* v[i][j] = 1 means that disk i is in tower j */
134 
135 Biddy_Edge make_a_move(unsigned int size, unsigned int i, unsigned int j, unsigned int k);
136 Biddy_Edge compute_image(unsigned int size, Biddy_Edge R, Biddy_Edge T, Biddy_Edge cube);
137 
138 int main(int argc, char** argv) {
139 
140  unsigned int size;
141  Biddy_Edge I; /* the initial state BDD */
142  Biddy_Edge E,NOT_E; /* the final state BDD */
143  Biddy_Edge T; /* the transition relation */
144  Biddy_Edge R;
145  Biddy_Edge image;
146  unsigned int i, j;
147  int found, num_steps;
148  Biddy_Edge tmp1,tmp2;
149  Biddy_Edge cube;
150 
151  clock_t elapsedtime;
152 
153  if (argc > 1) {
154  sscanf(argv[1],"%u",&size);
155  if (size > MAXSIZE) {
156  printf("ERROR: MAXSIZE = %u\n",MAXSIZE);
157  exit(1);
158  }
159  } else {
160  size = SIZE;
161  }
162 
163  setbuf(stdout,NULL);
164  elapsedtime = clock();
165 
166  /* initialize the BDD manager with default options */
167 
168 #ifdef USE_BIDDY
169  printf("Using Biddy");
170  /* DEFAULT INIT CALL: Biddy_InitAnonymous(BIDDYTYPEOBDDC) */
171 #ifdef USE_OBDDC
172  Biddy_InitAnonymous(BIDDYTYPEOBDDC);
173 #elif USE_ZBDDC
174  Biddy_InitAnonymous(BIDDYTYPEZBDDC);
175 #elif USE_TZBDD
176  Biddy_InitAnonymous(BIDDYTYPETZBDD);
177 #else
178  Biddy_InitAnonymous(BIDDYTYPEOBDDC);
179 #endif
180 #endif
181 
182 #ifdef USE_CUDD
183  printf("Using CUDD");
184  /* DEFAULT INIT CALL: Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0) */
185  manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
186  /* Cudd_SetMaxCacheHard(manager,262144); */
187  /* Cudd_AutodynEnable(manager,CUDD_REORDER_SAME); */
188 #endif
189 
190  if (Biddy_GetManagerType() == BIDDYTYPEOBDDC) {
191  printf(" (OBDDC)...\n");
192  }
193  else if (Biddy_GetManagerType() == BIDDYTYPEZBDDC) {
194  printf(" (ZBDDC)...\n");
195  }
196  else if (Biddy_GetManagerType() == BIDDYTYPETZBDD) {
197  printf(" (TZBDD)...\n");
198  }
199  else {
200  printf(" (unknown)... EXIT!\n");
201  exit(1);
202  }
203 
204  /* create BDD variables */
205  /* the current and next state variables are interleaved */
206  /* this is usually a good ordering to start with */
207  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC) ||
208  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC))
209  {
210  char name[5];
211  name[0] = name[1] = name[2] = name[3] = name[4] = 0;
212  for(i=0;i<size;i++) {
213  name[1] = '0' + i/10;
214  name[2] = '0' + i%10;
215  for(j=0;j<3;j++) {
216  name[3] = '0' + j;
217  v1[i][j] = Biddy_AddVariable();
218  name[0] = 'C';
219  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
220  v2[i][j] = Biddy_AddVariable();
221  name[0] = 'N';
222  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
223  }
224  }
225  }
226 
227  /* for Biddy, ZBDD variables are added in the reverse order to get consistent results */
228  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC)) {
229 #ifdef USE_BIDDY
230  char name[5];
231  name[0] = name[1] = name[2] = name[3] = name[4] = 0;
232  for(i=0;i<size;i++) {
233  name[1] = '0' + (size-i-1)/10;
234  name[2] = '0' + (size-i-1)%10;
235  for(j=0;j<3;j++) {
236  name[3] = '0' + (3-j-1);
237  v2[size-i-1][3-j-1] = Biddy_AddVariable();
238  name[0] = 'N';
239  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
240  v1[size-i-1][3-j-1] = Biddy_AddVariable();
241  name[0] = 'C';
242  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
243  }
244  }
245 #endif
246 #ifdef USE_CUDD
247  for(i=0;i<size;i++) {
248  for(j=0;j<3;j++) {
249  v1[i][j] = Biddy_AddVariable();
250  v2[i][j] = Biddy_AddVariable();
251  }
252  }
253 #endif
254  }
255 
256  /* for ZBDDs, by adding new variables all the existing ones are changed */
257  /* after adding the last variable we have to refresh edges in v1 and v2 */
258  /* NOTE: for Biddy, ZBDD variables are added in the reverse order */
259  /* NOTE: user variables in Biddy start with index 1 */
260  /* NOTE: for CUDD, user variables start with index 0 */
261  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC)) {
262 #ifdef USE_BIDDY
263  for(i=0;i<size;i++) {
264  for(j=0;j<3;j++) {
265  v1[i][j] = Biddy_GetVariableEdge(2*(size*3-(i*3+j)));
266  v2[i][j] = Biddy_GetVariableEdge(2*(size*3-(i*3+j))-1);
267  }
268  }
269 #endif
270 #ifdef USE_CUDD
271  for(i=0;i<size;i++) {
272  for(j=0;j<3;j++) {
273  v1[i][j] = Cudd_zddIthVar(manager,2*(i*3+j));
274  v2[i][j] = Cudd_zddIthVar(manager,2*(i*3+j)+1);
275  }
276  }
277 #endif
278  }
279 
280  /* in the initial state, all the disks are in tower 0 */
281 
282  I = Biddy_GetConstantOne();
283 #ifdef USE_CUDD
284  Cudd_Ref(I);
285 #endif
286  for(i=0;i<size;i++) {
287  tmp1 = Biddy_And(I,v1[i][0]);
288 #ifdef USE_CUDD
289  Cudd_Ref(tmp1);
290  Cudd_RecursiveDeref(manager,I);
291 #endif
292  I = tmp1;
293  }
294  for(i=0;i<size;i++) {
295  tmp1 = Biddy_And(I,Biddy_Not(v1[i][1]));
296 #ifdef USE_CUDD
297  Cudd_Ref(tmp1);
298  Cudd_RecursiveDeref(manager,I);
299 #endif
300  I = tmp1;
301  }
302  for(i=0;i<size;i++) {
303  tmp1 = Biddy_And(I,Biddy_Not(v1[i][2]));
304 #ifdef USE_CUDD
305  Cudd_Ref(tmp1);
306  Cudd_RecursiveDeref(manager,I);
307 #endif
308  I = tmp1;
309  }
310 
311 #ifdef USE_BIDDY
312  Biddy_AddTmpFormula(I,1);
313  Biddy_Clean();
314 #endif
315 
316  /* in the final state, we want all the disks in tower 2 */
317 
318  E = Biddy_GetConstantOne();
319 #ifdef USE_CUDD
320  Cudd_Ref(E);
321 #endif
322  for(i=0;i<size;i++) {
323  tmp1 = Biddy_And(E,v1[i][2]);
324 #ifdef USE_CUDD
325  Cudd_Ref(tmp1);
326  Cudd_RecursiveDeref(manager,E);
327 #endif
328  E = tmp1;
329  }
330 
331  for(i=0;i<size;i++) {
332  tmp1 = Biddy_And(E,Biddy_Not(v1[i][0]));
333 #ifdef USE_CUDD
334  Cudd_Ref(tmp1);
335  Cudd_RecursiveDeref(manager,E);
336 #endif
337  E = tmp1;
338  }
339 
340  for(i=0;i<size;i++) {
341  tmp1 = Biddy_And(E,Biddy_Not(v1[i][1]));
342 #ifdef USE_CUDD
343  Cudd_Ref(tmp1);
344  Cudd_RecursiveDeref(manager,E);
345 #endif
346  E = tmp1;
347  }
348 
349  NOT_E = Biddy_Not(E);
350 
351 #ifdef USE_BIDDY
352  Biddy_AddTmpFormula(I,1);
353  Biddy_AddTmpFormula(NOT_E,1);
354  Biddy_Clean();
355 #endif
356 
357  /* the transition relation is the disjunction of all possible moves */
358 
359  T = Biddy_GetConstantZero();
360 #ifdef USE_CUDD
361  Cudd_Ref(T);
362 #endif
363 
364  for(i=0;i<size;i++) {
365  for(j=0;j<3;j++) {
366  tmp1 = make_a_move(size,i,j,(j+1)%3);
367  tmp2 = Biddy_Or(T,tmp1);
368 #ifdef USE_CUDD
369  Cudd_Ref(tmp2);
370  Cudd_RecursiveDeref(manager,tmp1);
371  Cudd_RecursiveDeref(manager,T);
372 #endif
373  T = tmp2;
374  tmp1 = make_a_move(size,i,j,(j+2)%3);
375  tmp2 = Biddy_Or(T,tmp1);
376 #ifdef USE_CUDD
377  Cudd_Ref(tmp2);
378  Cudd_RecursiveDeref(manager,tmp1);
379  Cudd_RecursiveDeref(manager,T);
380 #endif
381  T = tmp2;
382 #ifdef USE_BIDDY
383  Biddy_AddTmpFormula(I,1);
384  Biddy_AddTmpFormula(NOT_E,1);
385  Biddy_AddTmpFormula(T,1);
386  Biddy_Clean();
387 #endif
388  }
389  }
390 
391  /* cube of the current state variables, needed by bddAndAbstract */
392  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC) ||
393  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC))
394  {
395  cube = Biddy_GetConstantOne();
396 #ifdef USE_CUDD
397  Cudd_Ref(cube);
398 #endif
399  for(i=0;i<size;i++) {
400  for(j=0;j<3;j++) {
401  tmp1 = Biddy_And(cube,v1[i][j]);
402 #ifdef USE_CUDD
403  Cudd_Ref(tmp1);
404  Cudd_RecursiveDeref(manager,cube);
405 #endif
406  cube = tmp1;
407  }
408  }
409  }
410  else if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC)) {
411 #ifdef USE_BIDDY
412  cube = Biddy_GetBaseSet();
413  for(i=0;i<size;i++) {
414  for(j=0;j<3;j++) {
415  /* for Biddy, user variables start with index 1 */
416  /* for Biddy, ZBDD variables have been generated in the following order: */
417  /* (1)=v2[size-1][2], (2)=v1[size-1][2], (3)=v2[size-1][1], (4)=v1[size-1][1],..., (2*size*3)=v1[0][0] */
418  cube = Biddy_Change(cube,2*(i*3+j)+2);
419  }
420  }
421 #endif
422 #ifdef USE_CUDD
423  /* NOT IMPLEMENTED, YET */
424 #endif
425  }
426 
427 #ifdef USE_BIDDY
428  Biddy_AddTmpFormula(I,1);
429  Biddy_AddTmpFormula(NOT_E,1);
430  Biddy_AddTmpFormula(T,1);
431  Biddy_AddTmpFormula(cube,1);
432  Biddy_Clean();
433 #endif
434 
435  found = 0;
436  num_steps = 0;
437 
438  /* R contains the states reached so far, initialized to I */
439  R = I;
440 #ifdef USE_CUDD
441  Cudd_Ref(R);
442 #endif
443 
444  /* fixed point computation */
445  while(1) {
446 
447 #ifdef REPORT
448  if (num_steps % (size*size) == 0) {
449  printf(
450  "R in while loop (num_steps=%u): %u variables, %.0f minterms, %u nodes.\n",
451  num_steps,3*size,Biddy_CountMinterm(R,3*size),Biddy_NodeNumber(R)
452  );
453  }
454 #endif
455 
456 #ifdef USE_BIDDY
457  Biddy_AddTmpFormula(R,1);
458  Biddy_AddTmpFormula(NOT_E,1);
459  Biddy_AddTmpFormula(T,1);
460  Biddy_AddTmpFormula(cube,1);
461  Biddy_Clean();
462 #endif
463 
464  /* check if we reached the goal state */
465  tmp1 = Biddy_Or(NOT_E,R);
466 #ifdef USE_CUDD
467  Cudd_Ref(tmp1);
468 #endif
469  if (tmp1 == Biddy_GetConstantOne()) {
470  found = 1; /* goal reached */
471  break;
472  }
473 #ifdef USE_CUDD
474  Cudd_RecursiveDeref(manager,tmp1);
475 #endif
476 
477  /* compute the successors of the current state */
478  image = compute_image(size,R,T,cube);
479  num_steps++;
480 
481  /* check if we reached a new state */
482  /* NOTE: fixed point check, easy with BDDs as they are canonical */
483  tmp1 = Biddy_Or(Biddy_Not(image),R);
484 #ifdef USE_CUDD
485  Cudd_Ref(tmp1);
486 #endif
487  if (tmp1 == Biddy_GetConstantOne())
488  break; /* no new state reached */
489 #ifdef USE_CUDD
490  Cudd_RecursiveDeref(manager,tmp1);
491 #endif
492 
493  /* add the new states to the reached set */
494  tmp1 = Biddy_Or(image,R);
495 #ifdef USE_CUDD
496  Cudd_Ref(tmp1);
497  Cudd_RecursiveDeref(manager,R);
498  Cudd_RecursiveDeref(manager,image);
499 #endif
500 
501  R = tmp1;
502  }
503 
504 #ifdef REPORT
505  printf(
506  "R in while loop (num_steps=%u): %u variables, %.0f minterms, %u nodes.\n",
507  num_steps,3*size,Biddy_CountMinterm(R,3*size),Biddy_NodeNumber(R)
508  );
509 #endif
510 
511  /* DUMP RESULT USING GRAPHVIZ/DOT */
512  /*
513 #ifdef USE_BIDDY
514  Biddy_WriteDot("hanoi-biddy.dot",image,"r",-1,FALSE);
515 #elif USE_CUDD
516  {
517  FILE * fp;
518  fp = fopen("hanoi-cudd.dot","w");
519  Cudd_DumpDot(manager,1,&image,NULL,NULL,fp);
520  fclose(fp);
521  }
522 #endif
523  */
524 
525 #ifdef USE_CUDD
526  Cudd_RecursiveDeref(manager,tmp1);
527  Cudd_RecursiveDeref(manager,image);
528 #endif
529 
530  elapsedtime = clock()-elapsedtime;
531 
532  if (found) {
533  printf("Goal Reached in %d steps\n",num_steps);
534  }
535  else
536  printf("Goal not reached\n");
537 
538  /* we have problems with passing stdout in the case you compile this file */
539  /* with MINGW and use biddy.dll generated with Visual Studio. */
540  /* In such cases, please, use Biddy_PrintInfo(NULL) */
541 #ifdef REPORTX
542  Biddy_PrintInfo(stdout);
543 #endif
544 
545  fprintf(stderr,"clock() TIME = %.2f\n",elapsedtime/(1.0*CLOCKS_PER_SEC));
546 
547  /* free BDDs and the manager */
548 
549  /* EXIT */
550 #ifdef USE_BIDDY
551  Biddy_Exit();
552 #endif
553 #ifdef USE_CUDD
554  Cudd_RecursiveDeref(manager,cube);
555  Cudd_RecursiveDeref(manager,I);
556  Cudd_RecursiveDeref(manager,T);
557  Cudd_RecursiveDeref(manager,E);
558 #ifdef REPORT
559  printf("CUDD: nodes with non-zero reference counts: %d\n",Cudd_CheckZeroRef(manager));
560 #endif
561  Cudd_Quit(manager);
562 #endif
563 
564 }
565 
566 /* returns a BDD representing move of disk i from tower j to tower k */
567 Biddy_Edge make_a_move(unsigned int size, unsigned int i, unsigned int j,
568  unsigned int k)
569 {
570  Biddy_Edge result;
571  unsigned int l,m;
572  Biddy_Edge tmp1;
573  Biddy_Edge tmp2;
574 
575  result = v1[i][j]; /* disk i is in tower j */
576 #ifdef USE_CUDD
577  Cudd_Ref(result);
578 #endif
579 
580  /* this loop enforces that there is no smaller disk in tower j or tower k */
581  /* no smaller disk in tower j implies that the disk at hand is at the top */
582  /* no smaller disk in tower k implies that we can move the disk to tower k */
583  for(l=i-1;l>=0;l--) {
584  tmp1 = Biddy_And(result,Biddy_Not(v1[l][j]));
585 #ifdef USE_CUDD
586  Cudd_Ref(tmp1);
587  Cudd_RecursiveDeref(manager,result);
588 #endif
589  result = tmp1;
590 
591  tmp1 = Biddy_And(result,Biddy_Not(v1[l][k]));
592 #ifdef USE_CUDD
593  Cudd_Ref(tmp1);
594  Cudd_RecursiveDeref(manager,result);
595 #endif
596  result = tmp1;
597  }
598 
599  /* move the current disk to tower k */
600  tmp1 = Biddy_And(result,v2[i][k]);
601 #ifdef USE_CUDD
602  Cudd_Ref(tmp1);
603  Cudd_RecursiveDeref(manager,result);
604 #endif
605  result = tmp1;
606 
607  tmp1 = Biddy_And(result,Biddy_Not(v2[i][(k+1)%3]));
608 #ifdef USE_CUDD
609  Cudd_Ref(tmp1);
610  Cudd_RecursiveDeref(manager,result);
611 #endif
612  result = tmp1;
613 
614  tmp1 = Biddy_And(result,Biddy_Not(v2[i][(k+2)%3]));
615 #ifdef USE_CUDD
616  Cudd_Ref(tmp1);
617  Cudd_RecursiveDeref(manager,result);
618 #endif
619  result = tmp1;
620 
621  /* the other disks stay where they are */
622  for(l=0;l<size;l++) {
623  if (l!=i) {
624  for(m=0;m<3;m++) {
625 
626  tmp1 = Biddy_Xnor(v1[l][m],v2[l][m]);
627 #ifdef USE_CUDD
628  Cudd_Ref(tmp1);
629 #endif
630 
631  tmp2 = Biddy_And(result,tmp1);
632 #ifdef USE_CUDD
633  Cudd_Ref(tmp2);
634  Cudd_RecursiveDeref(manager,result);
635  Cudd_RecursiveDeref(manager,tmp1);
636 #endif
637 
638  result = tmp2;
639  }
640  }
641  }
642 
643  return result;
644 }
645 
646 /* given a set of states R and a transition relation T, returns the BDD */
647 /* for the states that can be reached in one step from R following T */
648 Biddy_Edge compute_image(unsigned int size, Biddy_Edge R, Biddy_Edge T,
649  Biddy_Edge cube)
650 {
651  Biddy_Edge result;
652  unsigned int i;
653  unsigned int j;
654  Biddy_Edge tmp1;
655 
656  /* the following Cudd function computes the conjunction of R and T; */
657  /* and quantifies out the variables in cube ( the current state variables ) */
658  result = Biddy_AndAbstract(R,T,cube);
659 #ifdef USE_CUDD
660  Cudd_Ref(result);
661 #endif
662 
663  /* DEBUGGING, ONLY */
664  /*
665  printf(
666  "compute_image after ANDABSTRACT: i=%d, j=%d, %u variables, %.0f minterms, %u nodes.\n",
667  i,j,3*size,Biddy_CountMinterm(result,3*size),Biddy_NodeNumber(result)
668  );
669  */
670 
671  /* rename the next state variables to the current state variables */
672  for(i=0;i<size;i++) {
673  for(j=0;j<3;j++) {
674  /* compose replaces v2[i][j] with v1[i][j] */
675  /* original: Cudd_bddCompose(manager,result,v1[i][j],2*(i*3+j)+1) */
676  /* for Biddy, user variables start with index 1 */
677  /* for Biddy, OBDD and TZBDD variables have been generated in the following order: */
678  /* (0)=v1[0][0], (1)=v2[0][0], (2)=v1[0][1], (3)=v2[0][1],..., (2*size*3-1)=v2[size-1][2] */
679  /* for Biddy, ZBDD variables have been generated in the following order: */
680  /* (1)=v2[size-1][2], (2)=v1[size-1][2], (3)=v2[size-1][1], (4)=v1[size-1][1],..., (2*size*3)=v1[0][0] */
681  /* for CUDD, user variables start with index 0 */
682  /* for CUDD, OBDD and ZBDD variables have been generated in the following order: */
683  /* (0)=v1[0][0], (1)=v2[0][0], (2)=v1[0][1], (3)=v2[0][1],..., (2*size*3-1)=v2[size-1][2] */
684 #ifdef USE_BIDDY
685  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC) ||
686  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC))
687  {
688  tmp1 = Biddy_Compose(result,v1[i][j],2*(i*3+j)+2);
689  }
690  else if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC))
691  {
692  tmp1 = Biddy_Compose(result,v1[i][j],2*(size*3-(i*3+j))-1);
693  }
694 #endif
695 #ifdef USE_CUDD
696  tmp1 = Biddy_Compose(result,v1[i][j],2*(i*3+j)+1);
697  Cudd_Ref(tmp1);
698  Cudd_RecursiveDeref(manager,result);
699 #endif
700  result = tmp1;
701 
702  /* DEBUGGING, ONLY */
703  /*
704  printf(
705  "compute_image: i=%d, j=%d, %u variables, %.0f minterms, %u nodes.\n",
706  i,j,3*size,Biddy_CountMinterm(result,3*size),Biddy_NodeNumber(result)
707  );
708  */
709 
710  }
711  }
712 
713  return result;
714 }
#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_Clean()
Definition: biddy.h:663
#define Biddy_Xnor(f, g)
Definition: biddy.h:547
#define Biddy_ChangeVariableName(v, x)
Definition: biddy.h:458
#define Biddy_Change(f, v)
Definition: biddy.h:635
#define Biddy_GetConstantOne()
Definition: biddy.h:381
#define Biddy_PrintInfo(f)
Definition: biddy.h:1004
#define Biddy_Or(f, g)
Definition: biddy.h:525
#define Biddy_AndAbstract(f, g, cube)
Definition: biddy.h:605
#define Biddy_GetBaseSet()
Definition: biddy.h:388
#define Biddy_Compose(f, g, v)
Definition: biddy.h:575
#define Biddy_NodeNumber(f)
Definition: biddy.h:781
#define Biddy_VariableTableNum()
Definition: biddy.h:796
#define Biddy_Not(f)
Definition: biddy.h:506
#define Biddy_GetConstantZero()
Definition: biddy.h:374
#define Biddy_Exit()
Definition: biddy.h:301
File biddy.h contains declaration of all external data structures.
char Biddy_Boolean
Definition: biddy.h:220
#define Biddy_GetVariableEdge(v)
Definition: biddy.h:408
char * Biddy_String
Definition: biddy.h:223