Biddy  1.7.4
An academic Binary Decision Diagrams package
biddy-example-independence.c
1 /* $Revision: 362 $ */
2 /* $Date: 2017-12-17 17:01:16 +0100 (ned, 17 dec 2017) $ */
3 /* This file (biddy-example-independence.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: */
10 /* gcc -DNOCONVERGE -DNOPROFILE -DUNIX -DBIDDY -DOBDDC -O2 -o biddy-example-independence biddy-example-independence.c biddy-example-independence-usa.c biddy-example-independence-europe.c -I. -L./bin -static -lbiddy -lgmp */
11 /* gcc -DCONVERGE -DNOPROFILE -DUNIX -DBIDDY -DOBDDC -O2 -o biddy-example-independence-converge biddy-example-independence.c biddy-example-independence-usa.c biddy-example-independence-europe.c -I. -L./bin -static -lbiddy -lgmp */
12 /* gcc -DNOCONVERGE -DNOPROFILE -DCUDD -DOBDDC -O2 -o cudd-example-independence biddy-example-independence.c biddy-example-independence-usa.c biddy-example-independence-europe.c -I ../cudd/include/ -L ../cudd/lib/ -lcudd -lm */
13 /* gcc -DCONVERGE -DNOPROFILE -DCUDD -DOBDDC -O2 -o cudd-example-independence-converge biddy-example-independence.c biddy-example-independence-usa.c biddy-example-independence-europe.c -I ../cudd/include/ -L ../cudd/lib/ -lcudd -lm */
14 
15 /* define CALCULATE_KERNELS 0 OR 1 */
16 /* define USA_NO or USA_YES */
17 /* define EUROPE_NO or EUROPE_YES */
18 #define CALCULATE_KERNELS 0
19 #define USA_YES
20 #define EUROPE_YES
21 
22 #include <stdio.h>
23 #include <string.h>
24 #include <ctype.h>
25 #include <time.h>
26 
27 #include "biddy-cudd.h"
28 
29 extern void setDataUSA(unsigned int *size, unsigned int ***usa, unsigned int **order, char **codes);
30 extern void setDataEurope(unsigned int *size, unsigned int ***europe, unsigned int **order, char **codes);
31 static void createGraph(unsigned int size, unsigned int **edge, Biddy_Edge *state, Biddy_Edge *graph);
32 static Biddy_Edge calculateIndependence(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph);
33 static Biddy_Edge calculateKernels(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph);
34 static void writeOrder(char *codes, unsigned int *order, unsigned int size);
35 
36 int main(int argc, char** argv) {
37  unsigned int i;
38  Biddy_Boolean complete;
39  Biddy_Edge tmp;
40  Biddy_Edge r1,r2;
41  unsigned int n1,n2;
42  char *userinput;
43  long long unsigned memoryinuse;
44 
45  clock_t elapsedtime;
46 
47 #ifdef USA_YES
48  unsigned int usaSize = 0;
49  unsigned int **usaEdge;
50  unsigned int *usaOrder;
51  char *usaCodes;
52  Biddy_Edge *usaState;
53  Biddy_Edge *usaGraph;
54 #endif
55 
56 #ifdef EUROPE_YES
57  unsigned int europeSize = 0;
58  unsigned int **europeEdge;
59  unsigned int *europeOrder;
60  char *europeCodes;
61  Biddy_Edge *europeState;
62  Biddy_Edge *europeGraph;
63 #endif
64 
65  setbuf(stdout, NULL);
66 
67 #ifdef USA_YES
68  setDataUSA(&usaSize,&usaEdge,&usaOrder,&usaCodes);
69 #endif
70 
71 #ifdef EUROPE_YES
72  setDataEurope(&europeSize,&europeEdge,&europeOrder,&europeCodes);
73 #endif
74 
75 #include "biddy-cudd.c" /* this will initialize BDD manager */
76 
77 #ifdef BIDDY
78  if (argc == 1) {
79  Biddy_SetManagerParameters(-1,-1,-1,-1,-1,-1,-1,-1);
80  }
81  else if (argc == 7) {
82  int gcr,gcrF,gcrX;
83  int rr,rrF,rrX;
84  sscanf(argv[1],"%d",&gcr);
85  sscanf(argv[2],"%d",&gcrF);
86  sscanf(argv[3],"%d",&gcrX);
87  sscanf(argv[4],"%d",&rr);
88  sscanf(argv[5],"%d",&rrF);
89  sscanf(argv[6],"%d",&rrX);
90  Biddy_SetManagerParameters(gcr/100.0,gcrF/100.0,gcrX/100.0,rr/100.0,rrF/100.0,rrX/100.0,-1,-1);
91  printf("%d, %d, %d, %d, %d, %d, ",gcr,gcrF,gcrX,rr,rrF,rrX);
92  }
93  else if (argc == 10) {
94  int gcr,gcrF,gcrX;
95  int rr,rrF,rrX;
96  int st,cst;
97  sscanf(argv[1],"%d",&gcr);
98  sscanf(argv[2],"%d",&gcrF);
99  sscanf(argv[3],"%d",&gcrX);
100  sscanf(argv[4],"%d",&rr);
101  sscanf(argv[5],"%d",&rrF);
102  sscanf(argv[6],"%d",&rrX);
103  sscanf(argv[7],"%d",&st);
104  sscanf(argv[8],"%d",&cst);
105  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);
106  printf("%d, %d, %d, %d, %d, %d, ",gcr,gcrF,gcrX,rr,rrF,rrX);
107  }
108  else {
109  printf("Wrong number of parameters!\n");
110  exit(0);
111  }
112 #endif
113 
114 #ifdef CUDD
115  Cudd_SetMaxCacheHard(manager,262144);
116 #endif
117 
118 #ifdef USA_YES
119  usaGraph = (Biddy_Edge *) malloc(usaSize*sizeof(Biddy_Edge *));
120  usaState = (Biddy_Edge *) malloc(usaSize*sizeof(Biddy_Edge *));
121 #endif
122 
123 #ifdef EUROPE_YES
124  europeGraph = (Biddy_Edge *) malloc(europeSize*sizeof(Biddy_Edge *));
125  europeState = (Biddy_Edge *) malloc(europeSize*sizeof(Biddy_Edge *));
126 #endif
127 
128  /* CREATE BDD VARIABLES */
129  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC))
130  {
131  i = 0;
132  complete = FALSE;
133  while (!complete) {
134  complete = TRUE;
135  tmp = Biddy_AddVariable();
136 #ifdef USA_YES
137  if (i < usaSize) {
138  usaState[usaOrder[i]] = tmp;
139  REF(usaState[usaOrder[i]]);
140  }
141  complete = complete && (i >= (usaSize-1));
142 #endif
143 #ifdef EUROPE_YES
144  if (i < europeSize) {
145  europeState[europeOrder[i]] = tmp;
146  REF(europeState[europeOrder[i]]);
147  }
148  complete = complete && (i >= (europeSize-1));
149 #endif
150  i++;
151  }
152  }
153 
154  /* NOTE for Biddy: ZBDD and TZBDD variables are added in the reverse order by default */
155  /* NOTE for Biddy: usaState[0] = europeState[0] and it is last added */
156  /* NOTE for CUDD: usaState[0] = europeState[0] and it is first added */
157  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC) ||
158  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDD))
159  {
160  i = 0;
161  complete = FALSE;
162  while (!complete) {
163  complete = TRUE;
164  tmp = Biddy_AddVariable();
165 #ifdef USA_YES
166  if (i < usaSize) {
167 #ifdef CUDD
168  usaState[usaOrder[i]] = tmp;
169  REF(usaState[usaOrder[i]]);
170 #endif
171 #ifdef BIDDY
172  usaState[usaOrder[usaSize-i-1]] = tmp;
173 #endif
174  }
175  complete = complete && (i >= (usaSize-1));
176 #endif
177 #ifdef EUROPE_YES
178  if (i < europeSize) {
179 #ifdef CUDD
180  europeState[europeOrder[i]] = tmp;
181  REF(europeState[europeOrder[i]]);
182 #endif
183 #ifdef BIDDY
184  europeState[europeOrder[europeSize-i-1]] = tmp;
185 #endif
186  }
187  complete = complete && (i >= (europeSize-1));
188 #endif
189  i++;
190  }
191  }
192 
193  /* For ZBDDs, by adding new variables all the existing ones are changed. */
194  /* Thus, after adding the last variable we have to refresh the array of variables. */
195  /* NOTE: Biddy_GetVariableEdge returns variables by the creation time, not by the order used in the BDD */
196  /* NOTE for Biddy: user variables start with index 1 */
197  /* NOTE for CUDD: user variables start with index 0 */
198  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC))
199  {
200 
201 #ifdef BIDDY
202  i = 0;
203  complete = FALSE;
204  while (!complete) {
205  complete = TRUE;
206 #ifdef USA_YES
207  if (i < usaSize) {
208  usaState[usaOrder[i]] = Biddy_GetVariableEdge(usaSize-i);
209  }
210  complete = complete && (i >= (usaSize-1));
211 #endif
212 #ifdef EUROPE_YES
213  if (i < europeSize) {
214  europeState[europeOrder[i]] = Biddy_GetVariableEdge(europeSize-i);
215  }
216  complete = complete && (i >= (europeSize-1));
217 #endif
218  i++;
219  }
220  Biddy_Purge(); /* remove unnecessary nodes, this is useful only for ZBDDs */
221 #endif
222 
223 #ifdef CUDD
224  i = 0;
225  complete = FALSE;
226  while (!complete) {
227  complete = TRUE;
228 #ifdef USA_YES
229  if (i < usaSize) {
230  DEREF(usaState[usaOrder[i]]);
231  usaState[usaOrder[i]] = Cudd_zddIthVar(manager,i);
232  REF(usaState[usaOrder[i]]);
233  }
234  complete = complete && (i >= (usaSize-1));
235 #endif
236 #ifdef EUROPE_YES
237  if (i < europeSize) {
238  DEREF(europeState[europeOrder[i]]);
239  europeState[europeOrder[i]] = Cudd_zddIthVar(manager,i);
240  REF(europeState[europeOrder[i]]);
241  }
242  complete = complete && (i >= (europeSize-1));
243 #endif
244  i++;
245  }
246 #endif
247 
248  }
249 
250  /* HERE, BDD OPERATIONS START AND THUS WE START TO MEASURE THE TIME */
251  elapsedtime = clock();
252 
253 #ifdef USA_YES
254  createGraph(usaSize,usaEdge,usaState,usaGraph);
255 #endif
256 
257 #ifdef EUROPE_YES
258  createGraph(europeSize,europeEdge,europeState,europeGraph);
259 #endif
260 
261  r1 = Biddy_GetConstantZero();
262  r2 = Biddy_GetConstantZero();
263  REF(r1);
264  REF(r2);
265 
266 #ifdef USA_YES
267  if (!CALCULATE_KERNELS) {
268  /* CALCULATING INDEPENDENCE SETS FOR USA */
269  DEREF(r1);
270  r1 = calculateIndependence(usaSize,usaState,usaGraph);
271  } else {
272  /* CALCULATING KERNELS (MAXIMUM INDEPENDENCE SETS) FOR USA */
273  DEREF(r1);
274  r1 = calculateKernels(usaSize,usaState,usaGraph);
275  }
276  MARK_X("usa",r1);
277  for (i=0; i<usaSize; i++) {
278  DEREF(usaGraph[i]);
279  }
280 #endif
281 
282 #ifdef EUROPE_YES
283  if (!CALCULATE_KERNELS) {
284  /* CALCULATING INDEPENDENCE SETS FOR EUROPE */
285  DEREF(r2);
286  r2 = calculateIndependence(europeSize,europeState,europeGraph);
287  } else {
288  /* CALCULATING KERNELS (MAXIMUM INDEPENDENCE SETS) FOR EUROPE */
289  DEREF(r2);
290  r2 = calculateKernels(europeSize,europeState,europeGraph);
291  }
292  MARK_X("europe",r2);
293  for (i=0; i<europeSize; i++) {
294  DEREF(europeGraph[i]);
295  }
296 #endif
297 
298  /* TO GET RELEVANT TIME FOR SIFTING WE REMOVE UNNECESSARY NODES */
299  /* this will remove all tmp formulae created by createGraph() */
300 #ifdef BIDDY
301  Biddy_Purge();
302 #endif
303 #ifdef CUDD
304  /* TO DO */
305 #endif
306 
307  userinput = strdup("...");
308  while (userinput[0] != 'x') {
309 
310  /* We have problems with passing stdout in the case you compile this file */
311  /* with MINGW and use biddy.dll generated with Visual Studio. */
312  /* In such cases, please, use Biddy_PrintInfo(NULL) */
313  if (userinput[0] == 'r') {
314  Biddy_PrintInfo(stdout);
315  }
316 
317  /* SIFTING */
318 #ifdef CONVERGE
319  if (userinput[0] == 's') Biddy_GlobalConvergedSifting();
320 #ifdef BIDDY
321 #ifdef USA_YES
322  if (userinput[0] == 'u') Biddy_Sifting(r1,TRUE);
323 #endif
324 #ifdef EUROPE_YES
325  if (userinput[0] == 'e') Biddy_Sifting(r2,TRUE);
326 #endif
327 #endif
328 #else
329  if (userinput[0] == 's') Biddy_GlobalSifting();
330 #ifdef BIDDY
331 #ifdef USA_YES
332  if (userinput[0] == 'u') Biddy_Sifting(r1,FALSE);
333 #endif
334 #ifdef EUROPE_YES
335  if (userinput[0] == 'e') Biddy_Sifting(r2,FALSE);
336 #endif
337 #endif
338 #endif
339  /* Biddy only: for TZBDD, sifting may change top node! */
340 #ifdef BIDDY
341 #ifdef USA_YES
342  if (!Biddy_FindFormula((Biddy_String)"usa",&i,&r1)) exit(99);
343 #endif
344 #ifdef EUROPE_YES
345  if (!Biddy_FindFormula((Biddy_String)"europe",&i,&r2)) exit(99);
346 #endif
347 #endif
348 
351 
352  if ((userinput[0] == 's')
353 #ifdef BIDDY
354 #ifdef USA_YES
355  || (userinput[0] == 'u')
356 #endif
357 #ifdef EUROPE_YES
358  || (userinput[0] == 'e')
359 #endif
360 #endif
361  ) {
362 #ifdef CONVERGE
363  printf("(CONVERGING SIFTING");
364 #ifdef BIDDY
365  if (userinput[0] == 'u') {
366  printf(" ON FUNCTION FOR USA");
367  }
368  if (userinput[0] == 'e') {
369  printf(" ON FUNCTION FOR EUROPE");
370  }
371 #endif
372 #ifdef PROFILE
373  printf("), ");
374 #else
375  printf(")\n");
376 #endif
377 #else
378  printf("(SIFTING");
379 #ifdef BIDDY
380  if (userinput[0] == 'u') {
381  printf(" ON FUNCTION FOR USA");
382  }
383  if (userinput[0] == 'e') {
384  printf(" ON FUNCTION FOR EUROPE");
385  }
386 #endif
387 #ifdef PROFILE
388  printf("), ");
389 #else
390  printf(")\n");
391 #endif
392 #endif
393  }
394 
395 #ifndef PROFILE
396  printf("Resulting function r1/r2 depends on %u/%u variables.\n",n1,n2);
397  printf("Resulting function r1/r2 has %.0f/%.0f minterms.\n",Biddy_CountMinterms(r1,n1),Biddy_CountMinterms(r2,n2));
398  printf("System has %u nodes / %lu live nodes.\n",Biddy_NodeTableNum(),Biddy_NodeTableNumLive());
399 #ifdef BIDDY
400  printf("%s",Biddy_GetManagerName());
401  printf(" for resulting function r1/r2 has %u/%u nodes (%u/%u nodes if using complement edges).\n",
403 #endif
404 #ifdef CUDD
405  printf("BDD for resulting function r1/r2 has %u/%u nodes (using complement edges).\n",Biddy_CountNodes(r1),Biddy_CountNodes(r2));
406 #endif
407 #ifdef BIDDY
408  printf("Variable swaps performed so far: %u\n",Biddy_NodeTableSwapNumber());
409 #endif
410 #ifdef CUDD
411  printf("Variable swaps performed so far: %.0f\n",Cudd_ReadSwapSteps(manager));
412 #endif
413 #endif
414 #ifndef PROFILE
415 #ifdef USA_YES
416  printf("Order for USA: ");
417  writeOrder(usaCodes,usaOrder,usaSize);
418 #endif
419 #ifdef EUROPE_YES
420  printf("Order for Europe: ");
421  writeOrder(europeCodes,europeOrder,europeSize);
422 #endif
423 #endif
424 #ifndef PROFILE
425 #ifdef BIDDY
426  printf("E[x]it or [r]eport or ");
427 #ifdef CONVERGE
428  printf("Converging sifting ");
429 #else
430  printf("Sifting ");
431 #endif
432 #if (defined USA_YES) || (defined EUROPE_YES)
433  printf("on [s]ystem or on function for");
434 #ifdef USA_YES
435  printf(" [u]SA");
436 #endif
437 #ifdef EUROPE_YES
438  printf(" [e]urope");
439 #endif
440 #endif
441 #endif
442 #ifdef CUDD
443  printf("E[x]it or [r]eport or ");
444 #ifdef CONVERGE
445  printf("Converging sifting ");
446 #else
447  printf("Sifting ");
448 #endif
449  printf("on [s]ystem");
450 #endif
451  printf(": ");
452 #endif
453 #ifdef PROFILE
454  if (!strcmp(userinput,"r")) userinput = strdup("x");
455  if (!strcmp(userinput,"s")) userinput = strdup("x");
456  if (!strcmp(userinput,"...")) userinput = strdup("s");
457 #else
458  if (!scanf("%s",userinput)) printf("ERROR\n");
459 #endif
460  }
461 
462  elapsedtime = clock()-elapsedtime;
463 
464  free(userinput);
465 
466  /* PROFILING */
467  memoryinuse = Biddy_ReadMemoryInUse();
468 #ifdef MINGW
469  fprintf(stderr,"%I64u, %u",memoryinuse,Biddy_NodeTableDRTime());
470 #else
471  fprintf(stderr,"%llu, %u",memoryinuse,(unsigned int)Biddy_NodeTableDRTime());
472 #endif
473  printf(", %u/%u",Biddy_CountNodes(r1),Biddy_CountNodes(r2));
474  fprintf(stderr,"\n");
475 
476  /* EXIT */
477 
478  DEREF(r1);
479  DEREF(r2);
480  for (i=0; i<usaSize; i++) {
481  DEREF(usaState[i]);
482  }
483  for (i=0; i<europeSize; i++) {
484  DEREF(europeState[i]);
485  }
486 
487 #ifdef CUDD
488  printf("CUDD: nodes with non-zero reference counts: %d\n",Cudd_CheckZeroRef(manager));
489 #endif
490 
491  Biddy_Exit();
492 }
493 
494 /* CREATE GRAPH */
495 static void createGraph(unsigned int size, unsigned int **edge, Biddy_Edge *state, Biddy_Edge *graph) {
496  unsigned int i,j;
497  Biddy_Edge tmp;
498  /*
499  printf("CREATE GRAPH... ");
500  */
501  for (i=0; i<size; i++) {
502  graph[i] = Biddy_GetConstantZero();
503  REF(graph[i]);
504  for (j=0; j<size; j++) {
505  if (edge[i][j]) {
506  tmp = Biddy_Or(graph[i],state[j]);
507  REF(tmp);
508  DEREF(graph[i]);
509  graph[i] = tmp;
510  }
511  }
512  MARK_0(graph[i]);
513  }
514  /*
515  printf("OK\n");
516  */
517 }
518 
519 /* CALCULATE INDEPENDENCE SETS */
520 static Biddy_Edge calculateIndependence(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph) {
521  unsigned int i;
522  Biddy_Edge p,r,tmp;
523  /*
524  printf("CALCULATE INDEPENDENCE SETS...\n");
525  */
526  r = Biddy_GetConstantZero();
527  REF(r);
528  for (i=0; i<size; i++) {
529  p = Biddy_And(graph[i],state[i]);
530  REF(p);
531  tmp = Biddy_Or(r,p);
532  MARK(tmp);
533  SWEEP();
534  REF(tmp);
535  DEREF(r);
536  DEREF(p);
537  r = tmp;
538  }
539  tmp = Biddy_Not(r);
540  MARK(tmp);
541  SWEEP();
542  REF(tmp);
543  DEREF(r);
544  r = tmp;
545  return r;
546 }
547 
548 /* CALCULATE KERNELS (MAXIMUM INDEPENDENCE SETS) */
549 static Biddy_Edge calculateKernels(unsigned int size, Biddy_Edge *state, Biddy_Edge *graph) {
550  unsigned int i;
551  Biddy_Edge p,r,tmp;
552  /*
553  printf("CALCULATE KERNELS (MAXIMUM INDEPENDENCE SETS)...\n");
554  */
555  r = Biddy_GetConstantZero();
556  REF(r);
557  for (i=0; i<size; i++) {
558  p = Biddy_Xnor(graph[i],state[i]);
559  REF(p);
560  tmp = Biddy_Or(r,p);
561  MARK(tmp);
562  SWEEP();
563  REF(tmp);
564  DEREF(r);
565  DEREF(p);
566  r = tmp;
567  }
568  tmp = Biddy_Not(r);
569  MARK(tmp);
570  SWEEP();
571  REF(tmp);
572  DEREF(r);
573  r = tmp;
574  return r;
575 }
576 
577 static void writeOrder(char *codes, unsigned int *order, unsigned int size) {
578  char ch;
579  unsigned int i;
580 #ifdef CUDD
581  int j;
582 #endif
583  int k;
584  unsigned int numvar,ivar;
585  unsigned int first;
586 
587  numvar = Biddy_VariableTableNum();
588  first = 1;
589 
590  /* In Biddy, the first user variable is at index [1] */
591  /* In CUDD, the first user variable is at index [0] */
592 #ifdef BIDDY
593  for (i=1; i<numvar; i++) {
594  ivar = Biddy_GetIthVariable(i)-1;
595 #endif
596 #ifdef CUDD
597  for (i=0; i<numvar; i++) {
598  ivar = Biddy_GetIthVariable(i);
599 #endif
600  /*
601  printf("(ith:%u=%u)",i,ivar);
602  */
603  if (ivar >= size) continue;
604 
605 #ifdef BIDDY
606  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC))
607  {
608  k = 3*(order[ivar]);
609  }
610  else if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC) ||
611  (Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDD))
612  {
613  k = 3*(order[size-ivar-1]);
614  }
615  else {
616  printf("ERROR: Unsupported BDD type\n");
617  exit(1);
618  }
619 #endif
620 
621 #ifdef CUDD
622  k = 3*(order[ivar]);
623 #endif
624 
625  ch = codes[k+2];
626  codes[k+2] = 0;
627  if (first) {
628  first = 0;
629  } else {
630  printf(",");
631  }
632  printf("%s",&codes[k]);
633  codes[k+2] = ch;
634  }
635  printf("\n");
636 
637 }
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_Xnor(f, g)
Definition: biddy.h:735
#define Biddy_NodeTableNum()
Definition: biddy.h:914
#define Biddy_DependentVariableNumber(f)
Definition: biddy.h:1054
#define Biddy_PrintInfo(f)
Definition: biddy.h:1091
#define Biddy_Or(f, g)
Definition: biddy.h:713
#define Biddy_FindFormula(x, idx, f)
Definition: biddy.h:616
#define Biddy_VariableTableNum()
Definition: biddy.h:889
#define Biddy_NodeTableSwapNumber()
Definition: biddy.h:964
#define Biddy_Not(f)
Definition: biddy.h:694
#define Biddy_NodeTableDRTime()
Definition: biddy.h:974
#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_SetManagerParameters(gcr, gcrF, gcrX, rr, rrF, rrX, st, cst)
Definition: biddy.h:331
#define Biddy_GetIthVariable(i)
Definition: biddy.h:415
#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