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