Biddy  1.7.4
An academic Binary Decision Diagrams package
biddy-example-hanoi.c
1 /* $Revision: 353 $ */
2 /* $Date: 2017-12-07 13:25:28 +0100 (čet, 07 dec 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 copyed from the 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 /* This example uses biddy-cudd.h and biddy-cudd.c */
17 
18 /* COMPILE WITH: */
19 /* gcc -DREPORT -DUNIX -DBIDDY -DOBDD -O2 -o biddy-example-hanoi-obdd biddy-example-hanoi.c -I. -L./bin -static -lbiddy -lgmp */
20 /* gcc -DREPORT -DUNIX -DBIDDY -DOBDDC -O2 -o biddy-example-hanoi-obddc biddy-example-hanoi.c -I. -L./bin -static -lbiddy -lgmp */
21 /* gcc -DREPORT -DUNIX -DBIDDY -DZBDDC -O2 -o biddy-example-hanoi-zbddc biddy-example-hanoi.c -I. -L./bin -static -lbiddy -lgmp */
22 /* gcc -DREPORT -DUNIX -DBIDDY -DTZBDD -O2 -o biddy-example-hanoi-tzbdd biddy-example-hanoi.c -I. -L./bin -static -lbiddy -lgmp */
23 /* gcc -DREPORT -DCUDD -DOBDDC -O2 -o cudd-example-hanoi-obddc biddy-example-hanoi.c -I ../cudd/include/ -L ../cudd/lib/ -lcudd -lm */
24 
25 /* Here are the original comments */
26 /*
27 This example essentially illustrates reachability computation, which
28 is one of the core operations inside a model checker. In model
29 checking, the goal state represents the error state, and the model
30 checker either:
31 1. Discovers that the error state is unreachable if the fixed point is
32  achieved before hitting the error.
33 2. Discovers that the error is reachable. In that case it returns a
34  counterexample, which is a sequence of steps from the initial state
35  to the error state.
36 The above implementation does not produce a counterexample.
37 Exercise: Add counterexample generation to the above.
38 How:
39 You will need to store pointers to all the image BDDs. Starting from
40 the error state, compute a "reverse image", intersect with the
41 correspoding forward image, pick a state from the intersection and
42 repeat till you hit the initial state.
43 */
44 
45 /* Towers of Hanoi problem using BDDs */
46 /* number of towers = 3 */
47 /* number of disks = SIZE */
48 #define MAXSIZE 16
49 #define SIZE 10
50 
51 #include <stdio.h>
52 #include <string.h>
53 #include <ctype.h>
54 #include <time.h>
55 
56 #include "biddy-cudd.h"
57 
58 Biddy_Edge v1[MAXSIZE][3]; /* the current state */
59 Biddy_Edge v2[MAXSIZE][3]; /* the next state */
60 
61 /* v[i][j] = 1 means that disk i is in tower j */
62 
63 Biddy_Edge make_a_move(unsigned int size, unsigned int i, unsigned int j, unsigned int k);
64 Biddy_Edge compute_image(unsigned int size, Biddy_Edge R, Biddy_Edge T, Biddy_Edge cube);
65 
66 int main(int argc, char** argv) {
67 
68  unsigned int size;
69  Biddy_Edge I; /* the initial state BDD */
70  Biddy_Edge E,NOT_E; /* the final state BDD */
71  Biddy_Edge T; /* the transition relation */
72  Biddy_Edge R;
73  Biddy_Edge image;
74  unsigned int i, j;
75  int found, num_steps;
76  Biddy_Edge tmp1,tmp2;
77  Biddy_Edge cube;
78 
79  clock_t elapsedtime;
80 
81  if (argc > 1) {
82  sscanf(argv[1],"%u",&size);
83  if (size > MAXSIZE) {
84  printf("ERROR: MAXSIZE = %u\n",MAXSIZE);
85  exit(1);
86  }
87  } else {
88  size = SIZE;
89  }
90 
91  setbuf(stdout,NULL);
92  elapsedtime = clock();
93 
94 #include "biddy-cudd.c" /* this will initialize BDD manager */
95 
96 #ifdef CUDD
97  /* Cudd_SetMaxCacheHard(manager,262144); */
98  /* Cudd_AutodynEnable(manager,CUDD_REORDER_SAME); */
99 #endif
100 
101  printf("%s",Biddy_GetManagerName());
102  if (Biddy_GetManagerType() == BIDDYTYPEOBDD) {
103  printf(" (OBDD)\n");
104  }
105  else if (Biddy_GetManagerType() == BIDDYTYPEOBDDC) {
106  printf(" (OBDDC)\n");
107  }
108  else if (Biddy_GetManagerType() == BIDDYTYPEZBDDC) {
109  printf(" (ZBDDC)\n");
110  }
111  else if (Biddy_GetManagerType() == BIDDYTYPETZBDD) {
112  printf(" (TZBDD)\n");
113  }
114  else {
115  printf(" (unknown)... EXIT!\n");
116  exit(1);
117  }
118 
119  /* create BDD variables */
120  /* the current and next state variables are interleaved */
121  /* this is usually a good ordering to start with */
122  /* Biddy allows state names, in CUDD we simply ignore them */
123  /* NOTE for Biddy: ZBDD and TZBDD variables are added in the reverse order by default */
124 
125 #ifdef BIDDY
126  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC))
127 #endif
128 #ifdef CUDD
129  if (TRUE)
130 #endif
131  {
132  char name[5];
133  name[0] = name[1] = name[2] = name[3] = name[4] = 0;
134  for(i=0;i<size;i++) {
135  name[1] = '0' + i/10;
136  name[2] = '0' + i%10;
137  for(j=0;j<3;j++) {
138  name[3] = '0' + j;
139  v1[i][j] = Biddy_AddVariable();
140  name[0] = 'C';
141  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
142  v2[i][j] = Biddy_AddVariable();
143  name[0] = 'N';
144  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
145  REF(v1[i][j]);
146  REF(v2[i][j]);
147  }
148  }
149  }
150 
151 #ifdef BIDDY
152  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC) ||
153  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC))
154 #endif
155 #ifdef CUDD
156  if (FALSE)
157 #endif
158  {
159  char name[5];
160  name[0] = name[1] = name[2] = name[3] = name[4] = 0;
161  for(i=0;i<size;i++) {
162  name[1] = '0' + (size-i-1)/10;
163  name[2] = '0' + (size-i-1)%10;
164  for(j=0;j<3;j++) {
165  name[3] = '0' + (3-j-1);
166  v2[size-i-1][3-j-1] = Biddy_AddVariable();
167  name[0] = 'N';
168  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
169  v1[size-i-1][3-j-1] = Biddy_AddVariable();
170  name[0] = 'C';
171  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
172  REF(v2[size-i-1][3-j-1]);
173  REF(v1[size-i-1][3-j-1]);
174  }
175  }
176  }
177 
178  /* For ZBDDs, by adding new variables all the existing ones are changed. */
179  /* Thus, after adding the last variable we have to refresh the array of variables. */
180  /* NOTE: Biddy_GetVariableEdge returns variables by the creation time, not by the order used in the BDD */
181  /* NOTE for Biddy: user variables start with index 1 */
182  /* NOTE for CUDD: user variables start with index 0 */
183 
184  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC)) {
185  for(i=0;i<size;i++) {
186  for(j=0;j<3;j++) {
187 #ifdef BIDDY
188  /* variable edges in Biddy never become obsolete */
189  v1[i][j] = Biddy_GetVariableEdge(2*(size*3-(i*3+j)));
190  v2[i][j] = Biddy_GetVariableEdge(2*(size*3-(i*3+j))-1);
191 #endif
192 #ifdef CUDD
193  /* variable edges in CUDD are referenced - this is required for ZBDDs */
194  DEREF(v1[i][j]);
195  DEREF(v2[i][j]);
196  v1[i][j] = Cudd_zddIthVar(manager,2*(i*3+j));
197  v2[i][j] = Cudd_zddIthVar(manager,2*(i*3+j)+1);
198  REF(v1[i][j]);
199  REF(v2[i][j]);
200 #endif
201  }
202  }
203  }
204 
205  /* DEBUGGING */
206  /**/
207 #ifdef BIDDY
208  {
209  Biddy_Variable v;
210  v = 0;
211  do {
212  v = Biddy_GetPrevVariable(v);
213  } while (!(Biddy_IsLowest(v)));
214  do {
215  printf("[%s]",Biddy_GetVariableName(v));
216  v = Biddy_GetNextVariable(v);
217  } while (v != 0);
218  printf("\n");
219  }
220 #endif
221  /**/
222 
223  /* in the initial state, all the disks are in tower 0 */
224 
225  I = Biddy_GetConstantOne();
226  REF(I);
227  for(i=0;i<size;i++) {
228  tmp1 = Biddy_And(I,v1[i][0]);
229  REF(tmp1);
230  DEREF(I);
231  I = tmp1;
232  }
233  for(i=0;i<size;i++) {
234  tmp1 = Biddy_And(I,Biddy_Not(v1[i][1]));
235  REF(tmp1);
236  DEREF(I);
237  I = tmp1;
238  }
239  for(i=0;i<size;i++) {
240  tmp1 = Biddy_And(I,Biddy_Not(v1[i][2]));
241  REF(tmp1);
242  DEREF(I);
243  I = tmp1;
244  }
245 
246  MARK(I);
247  SWEEP();
248 
249  /* in the final state, we want all the disks in tower 2 */
250 
251  E = Biddy_GetConstantOne();
252  REF(E);
253  for(i=0;i<size;i++) {
254  tmp1 = Biddy_And(E,v1[i][2]);
255  REF(tmp1);
256  DEREF(E);
257  E = tmp1;
258  }
259 
260  for(i=0;i<size;i++) {
261  tmp1 = Biddy_And(E,Biddy_Not(v1[i][0]));
262  REF(tmp1);
263  DEREF(E);
264  E = tmp1;
265  }
266 
267  for(i=0;i<size;i++) {
268  tmp1 = Biddy_And(E,Biddy_Not(v1[i][1]));
269  REF(tmp1);
270  DEREF(E);
271  E = tmp1;
272  }
273 
274  NOT_E = Biddy_Not(E);
275  REF(NOT_E);
276  DEREF(E);
277 
278  /* E is not needed anymore, only NOT_E is used further */
279 
280  MARK(I);
281  MARK(NOT_E);
282  SWEEP();
283 
284  /* the transition relation is the disjunction of all possible moves */
285 
286  T = Biddy_GetConstantZero();
287  REF(T);
288 
289  for(i=0;i<size;i++) {
290  for(j=0;j<3;j++) {
291 
292  tmp1 = make_a_move(size,i,j,(j+1)%3);
293 
294  tmp2 = Biddy_Or(T,tmp1);
295  REF(tmp2);
296  DEREF(tmp1);
297  DEREF(T);
298  T = tmp2;
299 
300  tmp1 = make_a_move(size,i,j,(j+2)%3);
301 
302  tmp2 = Biddy_Or(T,tmp1);
303  REF(tmp2);
304  DEREF(tmp1);
305  DEREF(T);
306  T = tmp2;
307 
308  MARK(I);
309  MARK(NOT_E);
310  MARK(T);
311  SWEEP();
312 
313  }
314  }
315 
316  /* cube of the current state variables, needed by bddAndAbstract */
317  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC) ||
318  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC))
319  {
320  cube = Biddy_GetConstantOne();
321  REF(cube);
322  for(i=0;i<size;i++) {
323  for(j=0;j<3;j++) {
324  tmp1 = Biddy_And(cube,v1[i][j]);
325  REF(tmp1);
326  DEREF(cube);
327  cube = tmp1;
328  }
329  }
330  }
331  else if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC)) {
332 #ifdef BIDDY
333  cube = Biddy_GetBaseSet();
334  for(i=0;i<size;i++) {
335  for(j=0;j<3;j++) {
336  /* for Biddy, user variables start with index 1 */
337  /* for Biddy, ZBDD variables have been generated in the following order: */
338  /* (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] */
339  cube = Biddy_Change(cube,2*(i*3+j)+2);
340  }
341  }
342 #endif
343 #ifdef CUDD
344  /* NOT IMPLEMENTED, YET */
345 #endif
346  }
347 
348  MARK(I);
349  MARK(NOT_E);
350  MARK(T);
351  MARK(cube);
352  SWEEP();
353 
354  found = 0;
355  num_steps = 0;
356 
357  /* R contains the states reached so far, initialized to I */
358  R = I;
359  REF(R);
360 
361  /* fixed point computation */
362  while(1) {
363 
364 #ifdef REPORT
365  if (num_steps % (size*size) == 0) {
366  printf(
367  "R in while loop (num_steps=%u): %u variables, %.0f minterms, %u nodes.\n",
369  );
370  }
371 #endif
372 
373  MARK(R);
374  MARK(NOT_E);
375  MARK(T);
376  MARK(cube);
377  SWEEP();
378 
379  /* check if we reached the goal state */
380  tmp1 = Biddy_Or(NOT_E,R);
381  if (tmp1 == Biddy_GetConstantOne()) {
382  found = 1; /* goal reached */
383  break;
384  }
385 
386  /* compute the successors of the current state */
387  image = compute_image(size,R,T,cube);
388  num_steps++;
389 
390  /* DEBUGGING */
391  /*
392  printf(
393  "image (num_steps=%u): %u variables, %.0f minterms, %u nodes.\n",
394  num_steps,Biddy_DependentVariableNumber(image),Biddy_CountMinterms(image,3*size),Biddy_CountNodes(image)
395  );
396  */
397 
398  /* check if we reached a new state */
399  /* NOTE: fixed point check, easy with BDDs as they are canonical */
400  tmp1 = Biddy_Not(image);
401  REF(tmp1);
402  tmp2 = Biddy_Or(tmp1,R);
403  REF(tmp2);
404  DEREF(tmp1);
405  if (tmp2 == Biddy_GetConstantOne()) {
406  DEREF(tmp2);
407  DEREF(image);
408  break; /* no new state reached */
409  }
410  DEREF(tmp2);
411 
412  /* add the new states to the reached set */
413  tmp1 = Biddy_Or(image,R);
414  REF(tmp1);
415  DEREF(image);
416  DEREF(R);
417  R = tmp1;
418 
419  }
420 
421 #ifdef REPORT
422  printf(
423  "R after while loop (num_steps=%u): %u variables, %.0f minterms, %u nodes.\n",
425  );
426 #endif
427 
428  /* DUMP RESULT USING GRAPHVIZ/DOT */
429  /*
430  Biddy_WriteDot("hanoi.dot",R,"R",-1,FALSE);
431  */
432 
433  elapsedtime = clock()-elapsedtime;
434 
435  if (found) {
436  printf("Goal Reached in %d steps\n",num_steps);
437  }
438  else
439  printf("Goal not reached\n");
440 
441  /* we have problems with passing stdout in the case you compile this file */
442  /* with MINGW and use biddy.dll generated with Visual Studio. */
443  /* In such cases, please, use Biddy_PrintInfo(NULL) */
444 #ifdef REPORTX
445  Biddy_PrintInfo(stdout);
446 #endif
447 
448  fprintf(stderr,"clock() TIME = %.2f\n",elapsedtime/(1.0*CLOCKS_PER_SEC));
449 
450  /* EXIT */
451 
452  DEREF(I);
453  DEREF(NOT_E);
454  DEREF(T);
455  DEREF(cube);
456  DEREF(R);
457  for(i=0;i<size;i++) {
458  for(j=0;j<3;j++) {
459  DEREF(v1[i][j]);
460  DEREF(v2[i][j]);
461  }
462  }
463 
464 #ifdef REPORT
465 #ifdef CUDD
466  printf("CUDD: nodes with non-zero reference counts: %d\n",Cudd_CheckZeroRef(manager));
467 #endif
468 #endif
469 
470  Biddy_Exit();
471 }
472 
473 /* returns a BDD representing move of disk i from tower j to tower k */
474 Biddy_Edge make_a_move(unsigned int size, unsigned int i, unsigned int j,
475  unsigned int k)
476 {
477  Biddy_Edge result;
478  unsigned int l,m;
479  Biddy_Edge tmp1;
480  Biddy_Edge tmp2;
481 
482  result = v1[i][j]; /* disk i is in tower j */
483  REF(result);
484 
485  /* this loop enforces that there is no smaller disk in tower j or tower k */
486  /* no smaller disk in tower j implies that the disk at hand is at the top */
487  /* no smaller disk in tower k implies that we can move the disk to tower k */
488  for(l=0;l<i;l++) {
489  tmp1 = Biddy_And(result,Biddy_Not(v1[l][j]));
490  REF(tmp1);
491  DEREF(result);
492  result = tmp1;
493 
494  tmp1 = Biddy_And(result,Biddy_Not(v1[l][k]));
495  REF(tmp1);
496  DEREF(result);
497  result = tmp1;
498  }
499 
500  /* move the current disk to tower k */
501  tmp1 = Biddy_And(result,v2[i][k]);
502  REF(tmp1);
503  DEREF(result);
504  result = tmp1;
505 
506  tmp1 = Biddy_And(result,Biddy_Not(v2[i][(k+1)%3]));
507  REF(tmp1);
508  DEREF(result);
509  result = tmp1;
510 
511  tmp1 = Biddy_And(result,Biddy_Not(v2[i][(k+2)%3]));
512  REF(tmp1);
513  DEREF(result);
514  result = tmp1;
515 
516  /* the other disks stay where they are */
517  for(l=0;l<size;l++) {
518  if (l!=i) {
519  for(m=0;m<3;m++) {
520 
521  tmp1 = Biddy_Xnor(v1[l][m],v2[l][m]);
522  REF(tmp1);
523 
524  tmp2 = Biddy_And(result,tmp1);
525  REF(tmp2);
526  DEREF(result);
527  DEREF(tmp1);
528 
529  result = tmp2;
530  }
531  }
532  }
533 
534  return result;
535 }
536 
537 /* given a set of states R and a transition relation T, returns the BDD */
538 /* for the states that can be reached in one step from R following T */
539 Biddy_Edge compute_image(unsigned int size, Biddy_Edge R, Biddy_Edge T,
540  Biddy_Edge cube)
541 {
542  Biddy_Edge result;
543  unsigned int i;
544  unsigned int j;
545  Biddy_Edge tmp1;
546 
547  /* the following Cudd function computes the conjunction of R and T; */
548  /* and quantifies out the variables in cube ( the current state variables ) */
549  result = Biddy_AndAbstract(R,T,cube);
550  REF(result);
551 
552  /* DEBUGGING, ONLY */
553  /*
554  printf(
555  "compute_image after ANDABSTRACT: i=%d, j=%d, %u variables, %.0f minterms, %u nodes.\n",
556  i,j,3*size,Biddy_CountMinterms(result,3*size),Biddy_CountNodes(result)
557  );
558  */
559 
560  /* rename the next state variables to the current state variables */
561  for(i=0;i<size;i++) {
562  for(j=0;j<3;j++) {
563  /* compose replaces v2[i][j] with v1[i][j] */
564  /* original: Cudd_bddCompose(manager,result,v1[i][j],2*(i*3+j)+1) */
565  /* for Biddy, user variables start with index 1 */
566  /* for Biddy, OBDD variables have been generated in the following order: */
567  /* (1)=v1[0][0], (2)=v2[0][0], (3)=v1[0][1], (4)=v2[0][1],..., (2*3*size)=v2[size-1][2] */
568  /* for Biddy, ZBDD and TZBDD variables have been generated in the following order: */
569  /* (1)=v2[size-1][2], (2)=v1[size-1][2], (3)=v2[size-1][1], (4)=v1[size-1][1],..., (2*3*size)=v1[0][0] */
570  /* for CUDD, user variables start with index 0 */
571  /* for CUDD, OBDD and ZBDD variables have been generated in the following order: */
572  /* (0)=v1[0][0], (1)=v2[0][0], (2)=v1[0][1], (3)=v2[0][1],..., (2*3*size-1)=v2[size-1][2] */
573 #ifdef BIDDY
574  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC))
575  {
576  tmp1 = Biddy_Compose(result,v1[i][j],2*(i*3+j)+2);
577  }
578  else if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC) ||
579  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC))
580  {
581  tmp1 = Biddy_Compose(result,v1[i][j],2*(size*3-(i*3+j))-1);
582  }
583 #endif
584 #ifdef CUDD
585  tmp1 = Biddy_Compose(result,v1[i][j],2*(i*3+j)+1);
586 #endif
587  REF(tmp1);
588  DEREF(result);
589  result = tmp1;
590 
591  /* DEBUGGING, ONLY */
592  /*
593  printf(
594  "compute_image: i=%d, j=%d, %u variables, %.0f minterms, %u nodes.\n",
595  i,j,3*size,Biddy_CountMinterms(result,3*size),Biddy_CountNodes(result)
596  );
597  */
598 
599  }
600  }
601 
602  return result;
603 }
#define Biddy_GetPrevVariable(v)
Definition: biddy.h:420
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_Xnor(f, g)
Definition: biddy.h:735
#define Biddy_ChangeVariableName(v, x)
Definition: biddy.h:510
#define Biddy_GetVariableName(v)
Definition: biddy.h:440
#define Biddy_DependentVariableNumber(f)
Definition: biddy.h:1054
#define Biddy_GetNextVariable(v)
Definition: biddy.h:425
#define Biddy_Change(f, v)
Definition: biddy.h:823
#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_AndAbstract(f, g, cube)
Definition: biddy.h:793
#define Biddy_GetBaseSet()
Definition: biddy.h:400
#define Biddy_Compose(f, g, v)
Definition: biddy.h:763
#define Biddy_VariableTableNum()
Definition: biddy.h:889
unsigned short int Biddy_Variable
Definition: biddy.h:253
#define Biddy_IsLowest(v)
Definition: biddy.h:495
#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_Exit()
Definition: biddy.h:313
#define Biddy_GetVariableEdge(v)
Definition: biddy.h:430
#define Biddy_CountNodes(f)
Definition: biddy.h:874
#define Biddy_GetManagerName()
Definition: biddy.h:326