Biddy  1.7.4
An academic Binary Decision Diagrams package
biddy-example-dictionary.c
1 /* $Revision: 353 $ */
2 /* $Date: 2017-12-07 13:25:28 +0100 (čet, 07 dec 2017) $ */
3 /* This file (biddy-example-dictionary.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 /* This example uses biddy-cudd.h and biddy-cudd.c */
9 
10 /* COMPILE WITH: */
11 /* gcc -DNOREPORT -DSIFTING -DUNIX -DBIDDY -DOBDDC -O2 -o biddy-example-dictionary biddy-example-dictionary.c -I. -L./bin -static -lbiddy -lgmp */
12 /* gcc -DNOREPORT -DSIFTING -DCUDD -DOBDDC -O2 -o cudd-example-dictionary biddy-example-dictionary.c -I ../cudd/include/ -L ../cudd/lib/ -lcudd -lm */
13 
14 /* THIS IS COMPATIBLE WITH D. E. Knuth's BENCHMARKS */
15 /**/
16 #define WORDSIZE 5
17 #define ALPHABETSIZE 26
18 #define ALPHABET {'A','B','C','D','E','F','G','H','I','J','K','L','M','N','O','P','Q','R','S','T','U','V','W','X','Y','Z'}
19 #define TOUPPER
20 #define FILENAME "./test/sgb-words.txt"
21 /**/
22 
23 /* THIS IS (ALMOST!?) COMPATIBLE WITH R. Bryant's BENCHMARKS */
24 /* NEWLINE IS THE LAST SYMBOL */
25 /*
26 #define WORDSIZE 24
27 #define ALPHABETSIZE 54
28 #define ALPHABET {'-', \
29  'A','B','C','D','E','F','G','H','I','J','K','L','M','N','O','P','Q','R','S','T','U','V','W','X','Y','Z', \
30  'a','b','c','d','e','f','g','h','i','j','k','l','m','n','o','p','q','r','s','t','u','v','w','x','y','z', \
31  '.' \
32  }
33 #define WITHNEWLINE
34 #define FILENAME "./test/words.txt"
35 */
36 
37 /* THIS IS (ALMOST!?) COMPATIBLE WITH R. Bryant's BENCHMARKS */
38 /* NEWLINE IS THE LAST SYMBOL */
39 /* BIDDY MUST BE ADAPTED TO SUPPORT THE HUGE NUMBER OF VARIABLES */
40 /*
41 #define WORDSIZE 24
42 #define ALPHABETSIZE 129
43 #define ALPHABET {}
44 #define ASCII
45 #define WITHNEWLINE
46 #define FILENAME "./test/words.txt"
47 */
48 
49 /* THIS IS FOR TESTING, ONLY */
50 /*
51 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
52 A B C Č D E F G H I J K L M N O P Q R S Š T U V W X Y Z Ž
53 */
54 /*
55 #define ALPHABET {'A','B','C','Č','D','E','F','G','H','I','J','K','L','M','N','O','P','R','S','Š','T','U','V','Z','Ž'}
56 #define ALPHABET {'A','B','C','Č','D','E','F','G','H','I','J','K','L','M','N','O','P','Q','R','S','Š','T','U','V','W','X','Y','Z','Ž'}
57 */
58 
59 #include <stdio.h>
60 #include <string.h>
61 #include <ctype.h>
62 #include <time.h>
63 
64 #include "biddy-cudd.h"
65 
66 /* BDD CREATION IS OPTIMIZED BY DEFAULT BUT YOU CAN OVERRIDE THIS */
67 #if !defined(BOTTOMUP) && !defined(TOPDOWN)
68 # if defined(OBDD) || defined(OBDDC)
69 # define BOTTOMUP
70 # endif
71 # if defined(ZBDD) || defined(ZBDDC)
72 # define TOPDOWN
73 # endif
74 # if defined(TZBDD) || defined(TZBDDC)
75 # define BOTTOMUP
76 # endif
77 #endif
78 
79 int main(int argv, char ** argc) {
80  clock_t elapsedtime;
81  FILE *f;
82  char alphabet[ALPHABETSIZE] = ALPHABET;
83  Biddy_Edge code[WORDSIZE][ALPHABETSIZE]; /* BDD variables */
84  Biddy_Edge codenot[WORDSIZE][ALPHABETSIZE]; /* BDD variables */
85  Biddy_Edge dictionary;
86  Biddy_Edge tmp1,tmp2;
87  unsigned int i,j,n;
88  unsigned int letter;
89  Biddy_String name;
90  char oneword[WORDSIZE+1]; /* word + \0 */
91  Biddy_Boolean eof,stop;
92  Biddy_String userinput;
93  unsigned int dictionary_idx;
94 
95  setbuf(stdout,NULL);
96  userinput = strdup("...");
97 
98 #include "biddy-cudd.c" /* this will initialize BDD manager */
99 
100  printf(" (%s)\n",Biddy_GetManagerName());
101 
102 #ifdef WITHNEWLINE
103  printf("USING NEW LINE\n");
104 #endif
105 
106 #ifdef REVERSEORDER
107  printf("USING REVERSE ORDER\n");
108 #endif
109 
110 #ifdef BOTTOMUP
111  printf("USING BOTTOM-UP APPROACH\n");
112 #endif
113 
114 #ifdef TOPDOWN
115  printf("USING TOP-DOWN APPROACH\n");
116 #endif
117 
118 #ifdef ASCII
119  for (i=0; i<ALPHABETSIZE; i++) {
120  alphabet[i] = i;
121  }
122 #endif
123 
124  /* check alphabet */
125  for (i=0; i<ALPHABETSIZE; i++) {
126  if ((alphabet[i] >= 32) && (alphabet[i] <= 126)) {
127  printf("(%c)",alphabet[i]);
128  } else {
129  printf("()");
130  }
131  }
132  printf("\n");
133 
134  elapsedtime = clock();
135 
136  /* create BDD variables */
137  /* NOTE for Biddy: ZBDD and TZBDD variables are added in the reverse order by default */
138  /* NOTE for Biddy and CUDD: in any case, code[0][0] = "A01" (i.e. the first letter in the alphabet) */
139 
140 #ifdef BIDDY
141 #ifdef REVERSEORDER
142  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC) ||
143  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC))
144 #else
145  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC))
146 #endif
147 #endif
148 
149 #ifdef CUDD
150 #ifdef REVERSEORDER
151  if (FALSE)
152 #else
153  if (TRUE)
154 #endif
155 #endif
156 
157  {
158  char name[4];
159  name[0] = name[1] = name[2] = 0;
160  name[3] = 0; /* end of string */
161  for (i=0; i<WORDSIZE; i++) {
162  name[1] = '0' + (i+1)/10;
163  name[2] = '0' + (i+1)%10;
164  for (j=0; j<ALPHABETSIZE; j++) {
165  name[0] = alphabet[j];
166  code[i][j] = Biddy_AddVariable();
167  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
168  REF(code[i][j]);
169  /* printf("(code[%u][%u]=%s)",i,j,name); */
170  }
171  }
172  }
173 
174 #ifdef BIDDY
175 #ifdef REVERSEORDER
176  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC))
177 #else
178  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC) ||
179  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC))
180 #endif
181 #endif
182 
183 #ifdef CUDD
184 #ifdef REVERSEORDER
185  if (TRUE)
186 #else
187  if (FALSE)
188 #endif
189 #endif
190 
191  {
192  char name[4];
193  name[0] = name[1] = name[2] = 0;
194  name[3] = 0; /* end of string */
195  for (i=0; i<WORDSIZE; i++) {
196  name[1] = '0' + (WORDSIZE-i)/10;
197  name[2] = '0' + (WORDSIZE-i)%10;
198  for (j=0; j<ALPHABETSIZE; j++) {
199  name[0] = alphabet[ALPHABETSIZE-j-1];
200  code[WORDSIZE-i-1][ALPHABETSIZE-j-1] = Biddy_AddVariable();
201  Biddy_ChangeVariableName(Biddy_VariableTableNum()-1,name); /* rename the last added variable */
202  REF(code[WORDSIZE-i-1][ALPHABETSIZE-j-1]);
203  /* printf("(code[%u][%u]=%s)",WORDSIZE-i-1,ALPHABETSIZE-j-1,name); */
204  }
205  }
206  }
207 
208  /* For ZBDDs, by adding new variables all the existing ones are changed. */
209  /* Thus, after adding the last variable we have to refresh the array of variables. */
210  /* NOTE: Biddy_GetVariableEdge returns variables by the creation time, not by the order used in the BDD */
211  /* NOTE for Biddy: user variables start with index 1 */
212  /* NOTE for CUDD: user variables start with index 0 */
213 
214  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC))
215  {
216  for (i=0; i<WORDSIZE; i++) {
217  for (j=0; j<ALPHABETSIZE; j++) {
218 #ifdef BIDDY
219  /* variable edges in Biddy never become obsolete */
220 #ifdef REVERSEORDER
221  code[i][j] = Biddy_GetVariableEdge(i*ALPHABETSIZE+j+1);
222 #else
223  code[i][j] = Biddy_GetVariableEdge(WORDSIZE*ALPHABETSIZE-(i*ALPHABETSIZE+j));
224 #endif
225 #endif
226 #ifdef CUDD
227  /* variable edges in CUDD are referenced - this is required for ZBDDs */
228  DEREF(code[i][j]);
229 #ifdef REVERSEORDER
230  code[i][j] = Biddy_GetVariableEdge(WORDSIZE*ALPHABETSIZE-(i*ALPHABETSIZE+j)-1);
231 #else
232  code[i][j] = Biddy_GetVariableEdge(i*ALPHABETSIZE+j);
233 #endif
234  REF(code[i][j]);
235 #endif
236  }
237  }
238  }
239 
240  /* CREATE NEGATIONS */
241  for (i=0; i<WORDSIZE; i++) {
242  for (j=0; j<ALPHABETSIZE; j++) {
243  codenot[i][j] = Biddy_Not(code[i][j]);
244  REF(codenot[i][j]);
245  MARK_0(codenot[i][j]);
246  }
247  }
248 
249  /* START CALCULATION */
250 
251 #ifdef TOPDOWN
252 #ifdef REVERSEORDER
253 # undef REVERSEORDER
254 #else
255 # define REVERSEORDER
256 #endif
257 #endif
258 
259  dictionary = Biddy_GetConstantZero();
260  REF(dictionary); /* not needed for Biddy but not wrong */
261 
262  /* DEBUGGING */
263  /**/
264  printf("\n");
265  printf("Initial system has %u nodes / %lu live nodes.\n",Biddy_NodeTableNum(),Biddy_NodeTableNumLive());
266 #ifdef BIDDY
267  printf("Initial system has %u user variables.\n",Biddy_VariableTableNum()-1);
268 #endif
269 #ifdef CUDD
270  printf("Initial system has %u user variables.\n",Biddy_VariableTableNum());
271 #endif
272  printf("Empty dictionary depends on %u variables.\n",Biddy_DependentVariableNumber(dictionary));
273  printf("Empty dictionary has %.0f minterms.\n",Biddy_CountMinterms(dictionary,WORDSIZE*ALPHABETSIZE));
274  printf("Empty dictionary has %u node(s).\n",Biddy_CountNodes(dictionary));
275  /**/
276 
277  n = 0;
278  f = fopen(FILENAME,"r");
279  eof = FALSE;
280  while (!eof) {
281  eof = ( fscanf(f,"%s",oneword) == EOF );
282  if (!eof) {
283  if (strlen(oneword) > WORDSIZE) {
284  printf("WORDSIZE TO SMALL, YOU NEED AT LEAST %u\n",(unsigned int)strlen(oneword));
285  exit(1);
286  }
287  n++;
288  tmp1 = Biddy_GetConstantOne();
289  REF(tmp1); /* not needed for Biddy but not wrong */
290 
291 /* IF NOT REVERSEORDER THEN ADD UNUSED VARIABLES FIRST BECAUSE THEY ARE AT THE BOTTOM PART OF THE BDD */
292 #ifndef REVERSEORDER
293  i = WORDSIZE-1;
294  while (i > strlen(oneword)) {
295  for (j=ALPHABETSIZE-1; j<ALPHABETSIZE; j--) { /* j is unsigned */
296  tmp2 = Biddy_And(tmp1,codenot[i][j]);
297  /* printf("AND[%u][%u]",i,j); */
298  REF(tmp2);
299  DEREF(tmp1);
300  tmp1 = tmp2;
301  }
302  i--;
303  }
304 #endif
305 
306 /* IF NOT REVERSEORDER THEN ADD NEWLINE VARIABLE BEFORE THE WORD BECAUSE THIS VARIABLE IS BOTTOM-MORE */
307 /* NEWLINE VARIABLE IS THE LAST VARIABLE IN THE ALPHABET */
308 #ifndef REVERSEORDER
309 #ifdef WITHNEWLINE
310  if (strlen(oneword) < WORDSIZE) {
311  j=ALPHABETSIZE-1;
312  tmp2 = Biddy_And(tmp1,code[i][j]);
313  /* printf("AND[%u][%u]",i,j); */
314  REF(tmp2);
315  DEREF(tmp1);
316  tmp1 = tmp2;
317  j--;
318  for (j; j<ALPHABETSIZE; j--) { /* j is unsigned */
319  tmp2 = Biddy_And(tmp1,codenot[i][j]);
320  /* printf("AND[%u][%u]",i,j); */
321  REF(tmp2);
322  DEREF(tmp1);
323  tmp1 = tmp2;
324  }
325  i--;
326  }
327 #endif
328 #endif
329 
330 /* ADD ALL LETTERS FROM THE WORD */
331 
332 #ifdef REVERSEORDER
333  for (i=0; i<strlen(oneword); i++) {
334 #else
335  for (i; i<strlen(oneword); i--) { /* i is unsigned */
336 #endif
337 
338 #ifdef TOUPPER
339  letter = toupper(oneword[i]);
340 #else
341  letter = oneword[i];
342 #endif
343 #ifdef REVERSEORDER
344  for (j=0; j<ALPHABETSIZE; j++) {
345 #else
346  for (j=ALPHABETSIZE-1; j<ALPHABETSIZE; j--) { /* j is unsigned */
347 #endif
348  if (letter == alphabet[j]) {
349  tmp2 = Biddy_And(tmp1,code[i][j]);
350  } else {
351  tmp2 = Biddy_And(tmp1,codenot[i][j]);
352  }
353  /* printf("AND[%u][%u]",i,j); */
354  REF(tmp2);
355  DEREF(tmp1);
356  tmp1 = tmp2;
357  }
358  }
359 
360 /* IF REVERSEORDER THEN ADD NEWLINE VARIABLE AFTER THE WORD BECAUSE THIS VARIABLE IS TOP-MORE */
361 /* NEWLINE VARIABLE IS THE LAST VARIABLE IN THE ALPHABET */
362 #ifdef REVERSEORDER
363 #ifdef WITHNEWLINE
364  if (i < WORDSIZE) {
365  for (j=0; j<ALPHABETSIZE-1; j++) {
366  tmp2 = Biddy_And(tmp1,codenot[i][j]);
367  /* printf("AND[%u][%u]",i,j); */
368  REF(tmp2);
369  DEREF(tmp1);
370  tmp1 = tmp2;
371  }
372  tmp2 = Biddy_And(tmp1,code[i][j]);
373  REF(tmp2);
374  DEREF(tmp1);
375  tmp1 = tmp2;
376  /* printf("AND[%u][%u]",i,j); */
377  i++;
378  }
379 #endif
380 #endif
381 
382 /* IF REVERSEORDER THEN ADD UNUSED VARIABLES LAST BECAUSE THEY ARE AT THE TOP PART OF THE BDD */
383 #ifdef REVERSEORDER
384  while (i < WORDSIZE) {
385  for (j=0; j<ALPHABETSIZE; j++) {
386  tmp2 = Biddy_And(tmp1,codenot[i][j]);
387  /* printf("AND[%u][%u]",i,j); */
388  REF(tmp2);
389  DEREF(tmp1);
390  tmp1 = tmp2;
391  }
392  i++;
393  }
394 #endif
395  /* printf("OR\n"); */
396 
397  tmp2 = Biddy_Or(dictionary,tmp1);
398  REF(tmp2);
399  DEREF(dictionary);
400  DEREF(tmp1);
401  dictionary = tmp2;
402 
403  MARK(dictionary);
404  SWEEP();
405 
406  /* DEBUGGING */
407  /* Biddy uses Biddy_CountNodesPlain() to report ZBDD nodes instead of ZBDDC nodes */
408  /*
409 #ifdef BIDDY
410  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC))
411  printf("<%s, nodes=%u / all=%u / live=%lu>\n",oneword,Biddy_CountNodesPlain(dictionary),Biddy_CountNodesNum(),Biddy_NodeTableNumLive());
412  else
413  printf("<%s, nodes=%u / all=%u / live=%lu>\n",oneword,Biddy_CountNodes(dictionary),Biddy_CountNodesNum(),Biddy_NodeTableNumLive());
414 #endif
415 #ifdef CUDD
416  printf("<%s, nodes=%u / all=%u / live=%lu>\n",oneword,Biddy_CountNodes(dictionary),Biddy_NodeTableNum(),Biddy_NodeTableNumLive());
417 #endif
418  */
419 
420  }
421  eof = (fgetc(f) == EOF);
422  }
423  fclose(f);
424  printf("%u WORDS READ FROM FILE %s\n",n,FILENAME);
425 
426  elapsedtime = clock()-elapsedtime;
427 
428 #ifdef SIFTING
429 #ifdef BIDDY
430  dictionary_idx = Biddy_AddPersistentFormula("DICT",dictionary);
431  Biddy_Purge(); /* dictionary_idx may change during purge */
432  Biddy_FindFormula("DICT",&dictionary_idx,&dictionary);
433 #endif
434 #endif
435 
436  do {
437 
438  /* FOR TZBDD, TOP EDGE OF dictionary MAY CHANGE DURING THE SIFTING */
439 #ifdef BIDDY
440  dictionary = Biddy_GetIthFormula(dictionary_idx);
441 #endif
442 
443  printf("\n");
444  printf("System has %u nodes / %lu live nodes.\n",Biddy_NodeTableNum(),Biddy_NodeTableNumLive());
445 #ifdef BIDDY
446  printf("System has %u user variables.\n",Biddy_VariableTableNum()-1);
447 #endif
448 #ifdef CUDD
449  printf("System has %u user variables.\n",Biddy_VariableTableNum());
450 #endif
451  printf("Resulting dictionary depends on %u variables.\n",Biddy_DependentVariableNumber(dictionary));
452  printf("Resulting dictionary has %.0f minterms.\n",Biddy_CountMinterms(dictionary,WORDSIZE*ALPHABETSIZE));
453  printf("Resulting dictionary has %u nodes.\n",Biddy_CountNodes(dictionary));
454 #ifdef BIDDY
455 #ifdef MINGW
456  printf("Memory in use: %I64u B\n",Biddy_ReadMemoryInUse());
457 #else
458  printf("Memory in use: %llu B\n",Biddy_ReadMemoryInUse());
459 #endif
460 #endif
461 #ifdef CUDD
462  printf("Memory in use: %lu B\n",Biddy_ReadMemoryInUse());
463 #endif
464 
465  printf("TIME: %.2f\n",elapsedtime/(1.0*CLOCKS_PER_SEC));
466 
467 #ifdef BIDDY
468  if (Biddy_GetManagerType() == BIDDYTYPEOBDD) {
469  printf("OBDD for resulting dictionary has %u nodes.\n",
470  Biddy_CountNodes(dictionary));
471  } else if (Biddy_GetManagerType() == BIDDYTYPEOBDDC) {
472  printf("OBDD for resulting dictionary has %u nodes (%u nodes if using complement edges).\n",
473  Biddy_CountNodesPlain(dictionary),Biddy_CountNodes(dictionary));
474  } else if (Biddy_GetManagerType() == BIDDYTYPEZBDD) {
475  printf("ZBDD for resulting dictionary has %u nodes.\n",
476  Biddy_CountNodes(dictionary));
477  } else if (Biddy_GetManagerType() == BIDDYTYPEZBDDC) {
478  printf("ZBDD for resulting dictionary has %u nodes (%u nodes if using complement edges).\n",
479  Biddy_CountNodesPlain(dictionary),Biddy_CountNodes(dictionary));
480  } else if (Biddy_GetManagerType() == BIDDYTYPETZBDD) {
481  printf("TZBDD for resulting dictionary has %u nodes.\n",
482  Biddy_CountNodes(dictionary));
483  } else if (Biddy_GetManagerType() == BIDDYTYPETZBDDC) {
484  printf("TZBDD for resulting dictionary has %u nodes (%u nodes if using complement edges).\n",
485  Biddy_CountNodesPlain(dictionary),Biddy_CountNodes(dictionary));
486  }
487 #endif
488 
489 #ifdef REPORT
490  Biddy_PrintInfo(stdout);
491 #endif
492 
493 #ifdef SIFTING
494  printf("SIFTING / CONVERGE SIFTING / EXIT [S/C/X]): ");
495  if (!scanf("%s",userinput)) printf("ERROR\n");
496 
497  elapsedtime = clock();
498 
499  if (toupper(userinput[0]) == 'S') {
500 #ifdef BIDDY
501  Biddy_Sifting(NULL,FALSE); /* global sifiting because no function is given, sifting is not converge */
502 #endif
503 #ifdef CUDD
504  Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT,0);
505 #endif
506  stop = FALSE;
507  } else if (toupper(userinput[0]) == 'C') {
508 #ifdef BIDDY
509  Biddy_Sifting(NULL,TRUE); /* global sifiting because no function is given, converge sifting */
510 #endif
511 #ifdef CUDD
512  Cudd_ReduceHeap(manager,CUDD_REORDER_SIFT_CONVERGE,0);
513 #endif
514  stop = FALSE;
515  } else if (toupper(userinput[0]) == 'X') {
516  stop = TRUE;
517  } else {
518  stop = FALSE;
519  }
520 #else
521  stop = TRUE;
522 #endif
523 
524  elapsedtime = clock()-elapsedtime;
525 
526  } while (!stop);
527 
528  free(userinput);
529 
530  /* DEBUGGING */
531  /*
532  printf("\n");
533  Biddy_WriteDot("dictionary.dot",dictionary,"DICT",-1,FALSE);
534  printf("USE 'dot -y -Tpng -O dictionary.dot' to visualize BDD for dictionary.\n");
535  */
536 
537  /* DEBUGGING */
538  /* THIS WILL GENERATE bddview FILE WITHOUT COORDINATES */
539  /* THIS FILE IS NOT SUPPORTED BY BDD Scout, YET */
540  /*
541  printf("\n");
542  Biddy_WriteBddview("dictionary.bddview",dictionary,"DICT",NULL);
543  */
544 
545  /* EXIT */
546 
547  DEREF(dictionary);
548  for (i=0; i<WORDSIZE; i++) {
549  for (j=0; j<ALPHABETSIZE; j++) {
550  DEREF(code[i][j]);
551  DEREF(codenot[i][j]);
552  }
553  }
554 
555 #ifdef REPORT
556 #ifdef CUDD
557  printf("CUDD: nodes with non-zero reference counts: %d\n",Cudd_CheckZeroRef(manager));
558 #endif
559 #endif
560 
561  Biddy_Exit();
562 
563 }
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_Purge()
Definition: biddy.h:575
#define Biddy_Sifting(f, c)
Definition: biddy.h:651
#define Biddy_NodeTableNum()
Definition: biddy.h:914
#define Biddy_ChangeVariableName(v, x)
Definition: biddy.h:510
#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_GetIthFormula(i)
Definition: biddy.h:631
#define Biddy_FindFormula(x, idx, f)
Definition: biddy.h:616
#define Biddy_VariableTableNum()
Definition: biddy.h:889
#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_CountNodesPlain(f)
Definition: biddy.h:1049
char Biddy_Boolean
Definition: biddy.h:232
#define Biddy_GetVariableEdge(v)
Definition: biddy.h:430
#define Biddy_ReadMemoryInUse()
Definition: biddy.h:1086
#define Biddy_CountNodes(f)
Definition: biddy.h:874
#define Biddy_GetManagerName()
Definition: biddy.h:326
char * Biddy_String
Definition: biddy.h:235