Biddy  1.7.4
An academic Binary Decision Diagrams package
biddy-example-random.c
1 /* $Revision: 353 $ */
2 /* $Date: 2017-12-07 13:25:28 +0100 (čet, 07 dec 2017) $ */
3 /* This file (biddy-example-random.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 */
8 
9 /* COMPILE WITH: */
10 /* gcc -DUNIX -O2 -o biddy-example-random biddy-example-random.c -I. -L./bin -static -lbiddy -lgmp */
11 
12 /* this example creates and converts random BDDs */
13 
14 #include "biddy.h"
15 
16 #define BOOLEANFUNCTION 1
17 #define COMBINATIONSET 2
18 
19 /* (POPULATION == -2): create one random function, only */
20 /* (POPULATION == -1): create one random function and perform tests */
21 /* (POPULATION == 0): not allowed */
22 /* (POPULATION > 0): create many random function and get statistics */
23 #define POPULATION -2
24 
25 #define SIZE 4
26 #define RATIO 0.5
27 
28 /* create Boolean function (BOOLEANFUNCTION) or combination set (COMBINATIONSET) */
29 #define RANDOMTYPE BOOLEANFUNCTION
30 
31 /* choose primary BDD type */
32 #define BDDTYPE BIDDYTYPEOBDDC
33 
34 int main() {
35  Biddy_Manager MNGOBDD,MNGZBDD,MNGTZBDD;
36  Biddy_Edge tmp,support,cube,result,result0,result1,result2;
37  Biddy_Edge robdd,rzbdd,rtzbdd;
38  Biddy_Variable v,first,last,extra;
39  unsigned int i;
40  unsigned int s1,s2,s3;
41 
42  unsigned int obddsize,zbddsize,tzbddsize;
43  unsigned int obddminsize,zbddminsize,tzbddminsize;
44  unsigned int obddmaxsize,zbddmaxsize,tzbddmaxsize;
45  unsigned int obddsmallest,zbddsmallest,tzbddsmallest;
46  unsigned int obddlargest,zbddlargest,tzbddlargest;
47  unsigned int allsamesize;
48 
49  if (POPULATION == 0) {
50  exit(1);
51  }
52 
53  if ((POPULATION == -1) || (POPULATION == -2)) {
54 
55  /* ************************************************************* */
56  /* START OF CREATION */
57  /* ************************************************************* */
58 
59  Biddy_InitAnonymous(BDDTYPE);
60 
61  Biddy_InitMNG(&MNGOBDD,BIDDYTYPEOBDDC);
62  Biddy_InitMNG(&MNGZBDD,BIDDYTYPEZBDDC);
63  Biddy_InitMNG(&MNGTZBDD,BIDDYTYPETZBDD);
64 
65  printf("Using %s...\n",Biddy_GetManagerName());
66 
67  /* for OBDDs, support is the most easiest calculated using AddVariable and AND */
68  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC)) {
69  tmp = Biddy_AddVariable();
70  support = tmp;
71  first = Biddy_GetTopVariable(tmp);
72  for (v=1; v<SIZE; v++) {
73  tmp = Biddy_AddVariable();
74  support = Biddy_And(support,tmp);
75  }
76  last = Biddy_GetTopVariable(tmp);
77  tmp = Biddy_AddVariable();
78  extra = Biddy_GetTopVariable(tmp);
79  }
80 
81 /* for ZBDDs, support is the most easiest calculated using AddElement and CHANGE */
82  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC)) {
83  tmp = Biddy_AddElement();
84  support = tmp;
85  first = Biddy_GetTopVariable(tmp);
86  for (v=1; v<SIZE; v++) {
87  tmp = Biddy_AddElement();
88  support = Biddy_Change(support,Biddy_GetTopVariable(tmp));
89  }
90  last = Biddy_GetTopVariable(tmp);
91  tmp = Biddy_AddElement();
92  extra = Biddy_GetTopVariable(tmp);
93  }
94 
95 /* for TZBDDs, the approaches from OBDDs and ZBDDs are both working, using the first one */
96  if ((Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC)) {
97  tmp = Biddy_AddVariable();
98  support = tmp;
99  first = Biddy_GetTopVariable(tmp);
100  for (v=1; v<SIZE; v++) {
101  tmp = Biddy_AddVariable();
102  support = Biddy_And(support,tmp);
103  }
104  last = Biddy_GetTopVariable(tmp);
105  tmp = Biddy_AddVariable();
106  extra = Biddy_GetTopVariable(tmp);
107  }
108 
109  /* GRAPHVIZ/DOT OUTPUT OF support - DEBUGGING, ONLY */
110  /*
111  if (SIZE < 10) {
112  Biddy_WriteDot("support.dot",support,"support",-1,FALSE);
113  printf("USE 'dot -y -Tpng -O support.dot' to visualize function support.\n");
114  }
115  */
116 
117  /* GENERATE RANDOM FUNCTION / COMBINATION SET */
118 
119  result = NULL;
120 
121 #if (RANDOMTYPE == BOOLEANFUNCTION)
122  printf("Generating random Boolean function...\n");
123  result = Biddy_RandomFunction(support,RATIO);
124 #endif
125 
126 #if (RANDOMTYPE == COMBINATIONSET)
127  printf("Generating random combination set...\n");
128  result = Biddy_RandomSet(support,RATIO);
129 #endif
130 
131  if (result == NULL) {
132  printf("ERROR: Function result is NULL!\n");
133  exit(1);
134  }
135 
136  /* TESTING */
137  /*
138  Biddy_Eval0("result B(0)(i(d(0)(y(0)(1)))(d(y(0)(1))(1)))");
139  Biddy_FindFormula("result",&i,&result);
140  Biddy_WriteDot("result.dot",result,"result",-1,FALSE);
141  printf("USE 'dot -y -Tpng -O result.dot' to visualize function result.\n");
142  Biddy_WriteBddview("result.bddview",result,"R",NULL);
143  exit(1);
144  */
145 
146  /* DEBUGGING */
147  /*
148  Biddy_Eval0("result 2(3(4(1)(*1))(4(*1)(1)))(3(4(*1)(1))(4(1)(*1)))");
149  Biddy_FindFormula("result",&i,&result);
150  */
151 
152  /* TRUTH TABLE AND GRAPH FOR THE RESULT - DEBUGGING, ONLY */
153  /*
154  if (SIZE < 10) {
155  printf("HERE IS A TRUTH TABLE FOR result:\n");
156  Biddy_PrintfTable(result);
157  }
158  Biddy_PrintfBDD(result);
159  */
160 
161  printf("Function result has %.0f minterms/combinations.\n",Biddy_CountMinterms(result,SIZE));
162  printf("Function result has density = %.2e.\n",Biddy_DensityOfFunction(result,SIZE));
163 
164  if (POPULATION == -2) exit(1);
165 
166  /* ************************************************************* */
167  /* START OF TESTING OPERATIONS */
168  /* ************************************************************* */
169 
170  /* OPERATION NOT */
171 
172  result0 = Biddy_Not(Biddy_Not(result));
173 
174  if (result0 != result) {
175  printf("ERROR: Operation NOT is wrong!\n");
176  }
177 
178  /* OPERATIONS AND/OR */
179 
180  result0 = Biddy_And(result,support);
181  result1 = Biddy_Not(Biddy_Or(Biddy_Not(result),Biddy_Not(support)));
182 
183  if (result0 != result1) {
184  printf("ERROR: Operations AND/OR are wrong!\n");
185  }
186 
187  /* OPERATIONS ITE/XOR */
188 
189  result0 = Biddy_ITE(result,Biddy_Not(support),support);
190  result1 = Biddy_Xor(result,support);
191 
192  if (result0 != result1) {
193  printf("ERROR: Operations ITE and/or XOR are wrong!\n");
194  }
195 
196  /* OPERATIONS LEQ AND GT */
197 
198  result0 = Biddy_Leq(result,support);
199  result1 = Biddy_Or(Biddy_Not(result),support);
200 
201  if (result0 != result1) {
202  printf("ERROR: Operation Leq is wrong!\n");
203  }
204 
205  result0 = Biddy_Leq(support,result);
206  result1 = Biddy_Or(Biddy_Not(support),result);
207 
208  if (result0 != result1) {
209  printf("ERROR: Operation Leq is wrong!\n");
210  }
211 
212  result0 = Biddy_Gt(result,support);
213  result1 = Biddy_And(result,Biddy_Not(support));
214 
215  if (result0 != result1) {
216  printf("ERROR: Operation Gt is wrong!\n");
217  }
218 
219  result0 = Biddy_Gt(support,result);
220  result1 = Biddy_And(support,Biddy_Not(result));
221 
222  if (result0 != result1) {
223  printf("ERROR: Operation Gt is wrong!\n");
224  }
225 
226  result0 = Biddy_Leq(result,support);
227  result1 = Biddy_Not(Biddy_Gt(result,support));
228 
229  if (result0 != result1) {
230  printf("ERROR: Operations Leq and/or Gt are wrong!\n");
231  }
232 
233  result0 = Biddy_Leq(support,result);
234  result1 = Biddy_Not(Biddy_Gt(support,result));
235 
236  if (result0 != result1) {
237  printf("ERROR: Operations Leq and/or Gt are wrong!\n");
238  }
239 
240  /* OPERATION SUBSET */
241 
242  result0 = Biddy_Subset0(result,first);
243  result1 = Biddy_Subset1(result,first);
244 
245  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
246  /*
247  if (SIZE < 10) {
248  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
249  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
250  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
251  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
252  }
253  */
254 
255  printf("Function result has %.0f minterms/combinations where first variable/element is NEGATIVE/ABSENT.\n",Biddy_CountMinterms(result0,SIZE));
256  printf("Function result has %.0f minterms/combinations where first variable/element is POSITIVE/PRESENT.\n",Biddy_CountMinterms(result1,SIZE));
257 
258  s1 = (unsigned int) Biddy_CountMinterms(result,SIZE);
259  s2 = (unsigned int) Biddy_CountMinterms(result0,SIZE);
260  s3 = (unsigned int) Biddy_CountMinterms(result1,SIZE);
261 
262  if (s1 != (s2 + s3)) {
263  printf("ERROR: Operation Subset is wrong!\n");
264  }
265 
266  result0 = Biddy_Subset0(result,last);
267  result1 = Biddy_Subset1(result,last);
268 
269  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
270  /*
271  if (SIZE < 10) {
272  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
273  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
274  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
275  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
276  }
277  */
278 
279  printf("Function result has %.0f minterms/combinations where last variable/element is NEGATIVE/ABSENT.\n",Biddy_CountMinterms(result0,SIZE));
280  printf("Function result has %.0f minterms/combinations where last variable/element is POSITIVE/PRESENT.\n",Biddy_CountMinterms(result1,SIZE));
281 
282  s1 = (unsigned int) Biddy_CountMinterms(result,SIZE);
283  s2 = (unsigned int) Biddy_CountMinterms(result0,SIZE);
284  s3 = (unsigned int) Biddy_CountMinterms(result1,SIZE);
285 
286  if (s1 != (s2 + s3)) {
287  printf("ERROR: Operation Subset is wrong!\n");
288  }
289 
290  /* OPERATION RESTRICT */
291 
292  result0 = Biddy_Restrict(result,first,FALSE);
293  result1 = Biddy_Restrict(result,first,TRUE);
294 
295  printf("If first variable is restricted to FALSE, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result0,SIZE));
296  printf("If first variable is restricted to TRUE, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result1,SIZE));
297 
298  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
299  /*
300  if (SIZE < 10) {
301  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
302  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
303  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
304  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
305  }
306  */
307 
308  s1 = (unsigned int) Biddy_CountMinterms(result,SIZE);
309  s2 = (unsigned int) Biddy_CountMinterms(result0,SIZE);
310  s3 = (unsigned int) Biddy_CountMinterms(result1,SIZE);
311 
312  if ((s1 + s1) != (s2 + s3)) {
313  printf("ERROR: Operation Restrict is wrong!\n");
314  }
315 
316  result0 = Biddy_Restrict(result,last,FALSE);
317  result1 = Biddy_Restrict(result,last,TRUE);
318 
319  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
320  /*
321  if (SIZE < 10) {
322  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
323  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
324  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
325  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
326  }
327  */
328 
329  printf("If last variable is restricted to FALSE, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result0,SIZE));
330  printf("If last variable is restricted to TRUE, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result1,SIZE));
331 
332  s1 = (unsigned int) Biddy_CountMinterms(result,SIZE);
333  s2 = (unsigned int) Biddy_CountMinterms(result0,SIZE);
334  s3 = (unsigned int) Biddy_CountMinterms(result1,SIZE);
335 
336  if ((s1 + s1) != (s2 + s3)) {
337  printf("ERROR: Operation Restrict is wrong!\n");
338  }
339 
340  /* OPERATION REPLACE */
341 
344 
345  result0 = Biddy_Replace(result);
346 
349 
350  result1 = Biddy_Replace(result0);
351 
352  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
353  /*
354  if (SIZE < 10) {
355  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
356  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
357  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
358  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
359  }
360  */
361 
362  if (result1 != result) {
363  printf("ERROR: Operation Replace is wrong!\n");
364  }
365 
366  /* OPERATION QUANTIFICATION */
367 
368  result0 = Biddy_E(result,first);
369  result1 = Biddy_A(result,first);
370 
371  printf("After the existential quantification of first variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result0,SIZE));
372  printf("After the universal quantification of first variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result1,SIZE));
373 
374  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
375  /*
376  if (SIZE < 10) {
377  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
378  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
379  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
380  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
381  }
382  */
383 
384  s1 = (unsigned int) Biddy_CountMinterms(result,SIZE);
385  s2 = (unsigned int) Biddy_CountMinterms(result0,SIZE);
386  s3 = (unsigned int) Biddy_CountMinterms(result1,SIZE);
387 
388  if ((s1 + s1) != (s2 + s3)) {
389  printf("ERROR: Operation Quantification is wrong!\n");
390  }
391 
392  result0 = Biddy_E(result,last);
393  result1 = Biddy_A(result,last);
394 
395  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
396  /*
397  if (SIZE < 10) {
398  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
399  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
400  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
401  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
402  }
403  */
404 
405  printf("After the existential quantification of last variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result0,SIZE));
406  printf("After the universal quantification of last variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result1,SIZE));
407 
408  s1 = (unsigned int) Biddy_CountMinterms(result,SIZE);
409  s2 = (unsigned int) Biddy_CountMinterms(result0,SIZE);
410  s3 = (unsigned int) Biddy_CountMinterms(result1,SIZE);
411 
412  if ((s1 + s1) != (s2 + s3)) {
413  printf("ERROR: Operation Quantification is wrong!\n");
414  }
415 
416  /* OPERATION ABSTRACTION */
417 
418  /* calculate cube */
419 
420  if ((Biddy_GetManagerType() == BIDDYTYPEOBDD) || (Biddy_GetManagerType() == BIDDYTYPEOBDDC)) {
421  cube = Biddy_GetConstantOne();
422  cube = Biddy_And(cube,Biddy_GetVariableEdge(first));
423  cube = Biddy_And(cube,Biddy_GetVariableEdge(last));
424  cube = Biddy_And(cube,Biddy_GetVariableEdge(extra));
425  }
426 
427  if ((Biddy_GetManagerType() == BIDDYTYPEZBDD) || (Biddy_GetManagerType() == BIDDYTYPEZBDDC)) {
428  cube = Biddy_GetBaseSet();
429  cube = Biddy_Change(cube,first);
430  cube = Biddy_Change(cube,last);
431  cube = Biddy_Change(cube,extra);
432  }
433 
434  if ((Biddy_GetManagerType() == BIDDYTYPETZBDD) || (Biddy_GetManagerType() == BIDDYTYPETZBDDC)) {
435  cube = Biddy_GetConstantOne();
436  cube = Biddy_And(cube,Biddy_GetVariableEdge(first));
437  cube = Biddy_And(cube,Biddy_GetVariableEdge(last));
438  cube = Biddy_And(cube,Biddy_GetVariableEdge(extra));
439  }
440 
441  result1 = Biddy_E(result,first);
442  result1 = Biddy_E(result1,last);
443  result2 = Biddy_ExistAbstract(result,cube);
444 
445  printf("After the existential abstraction of first and last variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result2,SIZE));
446 
447  /* GRAPHVIZ/DOT OUTPUT OF RESULT1 - DEBUGGING, ONLY */
448  /*
449  if (SIZE < 10) {
450  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
451  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
452  }
453  */
454 
455  if (result1 != result2) {
456  printf("ERROR: Operation Abstraction is wrong!\n");
457  }
458 
459  result1 = Biddy_A(result,first);
460  result1 = Biddy_A(result1,last);
461  result2 = Biddy_UnivAbstract(result,cube);
462 
463  printf("After the universal abstraction of first and last variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result2,SIZE));
464 
465  /* GRAPHVIZ/DOT OUTPUT OF RESULT1 - DEBUGGING, ONLY */
466  /*
467  if (SIZE < 10) {
468  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
469  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
470  }
471  */
472 
473  if (result1 != result2) {
474  printf("ERROR: Operation Abstraction is wrong!\n");
475  }
476 
477  result0 = Biddy_E(result,first);
478  result1 = Biddy_E(Biddy_Not(result),last);
479  result2 = Biddy_And(result0,result1);
480  result2 = Biddy_ExistAbstract(result2,cube);
481  result1 = Biddy_AndAbstract(result0,result1,cube);
482 
483  printf("After the first user-defined abstraction, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result1,SIZE));
484 
485  if (result1 != result2) {
486  printf("ERROR: Operation Abstraction is wrong!\n");
487  }
488 
489  result0 = Biddy_A(result,first);
490  result1 = Biddy_A(Biddy_Not(result),last);
491  result1 = Biddy_AndAbstract(result0,result1,cube);
492 
493  printf("After the second user-defined abstraction, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result1,SIZE));
494 
495  if (result1 != Biddy_GetConstantZero()) {
496  printf("ERROR: Operation Abstraction is wrong!\n");
497  }
498 
499  /* BOOLEAN OPERATIONS AND OPERATION ITE */
500 
501  result1 = Biddy_ITE(Biddy_E(result,first),Biddy_E(result,last),Biddy_A(result,last));
502  result2 = Biddy_ITE(Biddy_A(result,first),Biddy_E(result,last),Biddy_A(result,last));
503 
504  printf("After the first ITE, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result1,SIZE));
505  printf("After the second ITE, function result has %.0f minterms/combinations\n",Biddy_CountMinterms(result2,SIZE));
506 
507  /* GRAPHVIZ/DOT OUTPUT OF RESULT1 AND RESULT2 - DEBUGGING, ONLY */
508  /*
509  if (SIZE < 10) {
510  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
511  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
512  Biddy_WriteDot("result2.dot",result2,"result2",-1,FALSE);
513  printf("USE 'dot -y -Tpng -O result2.dot' to visualize function result2.\n");
514  }
515  */
516 
517  if (result1 != Biddy_Xor(
518  Biddy_And(Biddy_E(result,first),Biddy_E(result,last)),
519  Biddy_And(Biddy_Not(Biddy_E(result,first)),Biddy_A(result,last))))
520  {
521  printf("ERROR: result1 for Boolean operations ITE-AND-XOR-NOT is wrong!\n");
522  }
523  if (result1 != Biddy_Or(
524  Biddy_And(Biddy_E(result,first),Biddy_E(result,last)),
525  Biddy_Gt(Biddy_A(result,last),Biddy_E(result,first))))
526  {
527  printf("ERROR: result1 for Boolean operations ITE-AND-OR-GT is wrong!\n");
528  }
529 
530  if (result2 != Biddy_Xor(
531  Biddy_And(Biddy_A(result,first),Biddy_E(result,last)),
532  Biddy_And(Biddy_Not(Biddy_A(result,first)),Biddy_A(result,last))))
533  {
534  printf("ERROR: result2 for Boolean operations ITE-AND-XOR-NOT is wrong!\n");
535  }
536  if (result2 != Biddy_Or(
537  Biddy_And(Biddy_A(result,first),Biddy_E(result,last)),
538  Biddy_Gt(Biddy_A(result,last),Biddy_A(result,first))))
539  {
540  printf("ERROR: result2 for Boolean operations ITE-AND-OR-GT is wrong!\n");
541  }
542 
543  /* ************************************************************* */
544  /* START OF CONVERSIONS AND STATISTICS */
545  /* ************************************************************* */
546 
547  printf("%s for function result has %u nodes (including terminals).\n",Biddy_GetManagerName(),Biddy_CountNodes(result));
548  printf("%s for function result has %u plain nodes (including terminals).\n",Biddy_GetManagerName(),Biddy_CountNodesPlain(result));
549  printf("%s for function result has %llu one-paths.\n",Biddy_GetManagerName(),Biddy_CountPaths(result));
550  printf("Function represented by %s depends on %u variables.\n",Biddy_GetManagerName(),Biddy_DependentVariableNumber(result));
551  printf("Considering the given set of variables, %s for function result has %.0f minterms/combinations.\n",Biddy_GetManagerName(),Biddy_CountMinterms(result,SIZE));
552  /* GRAPHVIZ/DOT OUTPUT OF THE RESULT */
553  if (SIZE < 10) {
554  Biddy_WriteDot("result.dot",result,"result",-1,FALSE);
555  printf("USE 'dot -y -Tpng -O result.dot' to visualize %s for function result.\n",Biddy_GetManagerName());
556  }
557 
558  /* CONVERT THE RESULT INTO OBDDC */
559  robdd = Biddy_Copy(MNGOBDD,result);
560  printf("OBDDC for function result has %u nodes (including terminal).\n",Biddy_Managed_CountNodes(MNGOBDD,robdd));
561  printf("OBDDC for function result has %u plain nodes (including both terminals).\n",Biddy_Managed_CountNodesPlain(MNGOBDD,robdd));
562  printf("OBDDC for function result has %llu one-paths.\n",Biddy_Managed_CountPaths(MNGOBDD,robdd));
563  printf("Function represented by OBDDC depends on %u variables.\n",Biddy_Managed_DependentVariableNumber(MNGOBDD,robdd));
564  printf("Considering the given set of variables, OBDDC for function result has %.0f minterms/combinations.\n",Biddy_Managed_CountMinterms(MNGOBDD,robdd,SIZE));
565  /* GRAPHVIZ/DOT OUTPUT OF THE RESULT */
566  if (SIZE < 10) {
567  Biddy_Managed_WriteDot(MNGOBDD,"obdd.dot",robdd,"obdd",-1,FALSE);
568  printf("USE 'dot -y -Tpng -O obdd.dot' to visualize %s for function result.\n",Biddy_Managed_GetManagerName(MNGOBDD));
569  }
570 
571  /* CONVERT THE RESULT INTO ZBDDC */
572  if (Biddy_GetManagerType() != BIDDYTYPETZBDDC) {
573  rzbdd = Biddy_Copy(MNGZBDD,result);
574  printf("ZBDDC for function result has %u nodes (including terminal).\n",Biddy_Managed_CountNodes(MNGZBDD,rzbdd));
575  printf("ZBDDC for function result has %u plain nodes (including both terminals).\n",Biddy_Managed_CountNodesPlain(MNGZBDD,rzbdd));
576  printf("ZBDDC for function result has %llu one-paths.\n",Biddy_Managed_CountPaths(MNGZBDD,rzbdd));
577  printf("Function represented by ZBDDC depends on %u variables.\n",Biddy_Managed_DependentVariableNumber(MNGZBDD,rzbdd));
578  printf("Considering the given set of variables, ZBDDC for function result has %.0f minterms/combinations.\n",Biddy_Managed_CountMinterms(MNGZBDD,rzbdd,SIZE));
579  /* GRAPHVIZ/DOT OUTPUT OF THE RESULT */
580  if (SIZE < 10) {
581  Biddy_Managed_WriteDot(MNGZBDD,"zbdd.dot",rzbdd,"zbdd",-1,FALSE);
582  printf("USE 'dot -y -Tpng -O zbdd.dot' to visualize %s for function result.\n",Biddy_Managed_GetManagerName(MNGZBDD));
583  }
584  }
585 
586  if (Biddy_GetManagerType() != BIDDYTYPEZBDDC) {
587  /* CONVERT THE RESULT INTO TZBDDs */
588  rtzbdd = Biddy_Copy(MNGTZBDD,result);
589  printf("TZBDD for function result has %u nodes (including the terminal).\n",Biddy_Managed_CountNodes(MNGTZBDD,rtzbdd));
590  printf("TZBDD for function result has %llu one-paths.\n",Biddy_Managed_CountPaths(MNGTZBDD,rtzbdd));
591  printf("Function represented by TZBDD depends on %u variables.\n",Biddy_Managed_DependentVariableNumber(MNGTZBDD,rtzbdd));
592  printf("Considering the given set of variables, TZBDD for function result has %.0f minterms/combinations.\n",Biddy_Managed_CountMinterms(MNGTZBDD,rtzbdd,SIZE));
593  /* GRAPHVIZ/DOT OUTPUT OF THE RESULT */
594  if (SIZE < 10) {
595  Biddy_Managed_WriteDot(MNGTZBDD,"tzbdd.dot",rtzbdd,"tzbdd",-1,FALSE);
596  printf("USE 'dot -y -Tpng -O tzbdd.dot' to visualize %s for function result.\n",Biddy_Managed_GetManagerName(MNGTZBDD));
597  }
598  }
599 
600  Biddy_Exit();
601  Biddy_ExitMNG(&MNGOBDD);
602  Biddy_ExitMNG(&MNGZBDD);
603  Biddy_ExitMNG(&MNGTZBDD);
604 
605  } else {
606 
607  obddsize = zbddsize = tzbddsize = 0;
608  obddminsize = zbddminsize = tzbddminsize = 0;
609  obddmaxsize = zbddmaxsize = tzbddmaxsize = 0;
610  obddsmallest = zbddsmallest = tzbddsmallest = 0;
611  obddlargest = zbddlargest = tzbddlargest = 0;
612  allsamesize = 0;
613 
614  for (i=0; i<POPULATION; i++) {
615 
616  Biddy_InitMNG(&MNGOBDD,BIDDYTYPEOBDDC);
617  Biddy_InitMNG(&MNGZBDD,BIDDYTYPEZBDDC);
618  Biddy_InitMNG(&MNGTZBDD,BIDDYTYPETZBDD);
619 
620  support = Biddy_Managed_GetConstantOne(MNGOBDD);
621  for (v=0; v<SIZE; v++) {
622  support = Biddy_Managed_And(MNGOBDD,support,Biddy_Managed_AddVariable(MNGOBDD));
623  }
624 
625  robdd = Biddy_Managed_RandomFunction(MNGOBDD,support,RATIO);
626  rzbdd = Biddy_Managed_Copy(MNGOBDD,MNGZBDD,robdd);
627  rtzbdd = Biddy_Managed_Copy(MNGOBDD,MNGTZBDD,robdd);
628 
629  s1 = Biddy_Managed_CountNodes(MNGOBDD,robdd);
630  s2 = Biddy_Managed_CountNodes(MNGZBDD,rzbdd);
631  s3 = Biddy_Managed_CountNodes(MNGTZBDD,rtzbdd);
632 
633  obddsize += s1;
634  zbddsize += s2;
635  tzbddsize += s3;
636 
637  if (obddminsize == 0) obddminsize = s1;
638  if (zbddminsize == 0) zbddminsize = s2;
639  if (tzbddminsize == 0) tzbddminsize = s3;
640 
641  if (s1 < obddminsize) obddminsize = s1;
642  if (s2 < zbddminsize) zbddminsize = s2;
643  if (s3 < tzbddminsize) tzbddminsize = s3;
644 
645  if (s1 > obddmaxsize) obddmaxsize = s1;
646  if (s2 > zbddmaxsize) zbddmaxsize = s2;
647  if (s3 > tzbddmaxsize) tzbddmaxsize = s3;
648 
649  if ((s1 < s2) && (s1 < s3)) obddsmallest++;
650  if ((s2 < s1) && (s2 < s3)) zbddsmallest++;
651  if ((s3 < s1) && (s3 < s2)) tzbddsmallest++;
652  if ((s1 == s2) && (s1 < s3)) tzbddlargest++;
653  if ((s1 == s3) && (s1 < s2)) zbddlargest++;
654  if ((s2 == s3) && (s2 < s1)) obddlargest++;
655  if ((s1 == s2) && (s2 == s3)) allsamesize++;
656 
657  /* TESTING: if ZBDD is the smallest */
658  /*
659  if ((s2 < s1) && (s2 < s3)) {
660  printf("OBDD has %u nodes without complemented edges (%u with complemented edges).\n",
661  Biddy_Managed_CountNodesPlain(MNGOBDD,robdd), Biddy_Managed_CountNodes(MNGOBDD,robdd));
662  printf("ZBDD has %u nodes without complemented edges (%u with complemented edges).\n",
663  Biddy_Managed_CountNodesPlain(MNGZBDD,rzbdd), Biddy_Managed_CountNodes(MNGZBDD,rzbdd));
664  printf("TZBDD has %u nodes without complemented edges.\n",
665  Biddy_Managed_CountNodes(MNGTZBDD,rtzbdd));
666  Biddy_Managed_PrintfTable(MNGOBDD,robdd);
667  Biddy_Managed_WriteDot(MNGOBDD,"obdd.dot",robdd,"obdd",-1,FALSE);
668  printf("USE 'dot -y -Tpng -O obdd.dot' to visualize OBDDC for function result.\n");
669  Biddy_Managed_WriteDot(MNGZBDD,"zbdd.dot",rzbdd,"zbdd",-1,FALSE);
670  printf("USE 'dot -y -Tpng -O zbdd.dot' to visualize ZBDDC for function result.\n");
671  Biddy_Managed_WriteDot(MNGTZBDD,"tzbdd.dot",rtzbdd,"tzbdd",-1,FALSE);
672  printf("USE 'dot -y -Tpng -O tzbdd.dot' to visualize TZBDD for function result.\n");
673  }
674  */
675 
676  Biddy_ExitMNG(&MNGOBDD);
677  Biddy_ExitMNG(&MNGZBDD);
678  Biddy_ExitMNG(&MNGTZBDD);
679 
680  }
681 
682  printf("RESULTS FOR POPULATION=%u, SIZE=%u, RATIO=%.2e\n",POPULATION,SIZE,RATIO);
683  printf("the average size of OBDDs = %.2f (min = %u, max = %u)\n",1.0*obddsize/POPULATION,obddminsize,obddmaxsize);
684  printf("the average size of ZBDDs = %.2f (min = %u, max = %u)\n",1.0*zbddsize/POPULATION,zbddminsize,zbddmaxsize);
685  printf("the average size of TZBDDs = %.2f (min = %u, max = %u)\n",1.0*tzbddsize/POPULATION,tzbddminsize,tzbddmaxsize);
686  printf("OBDD is the smallest in %u examples (%.2f%%)\n",obddsmallest,100.0*obddsmallest/POPULATION);
687  printf("ZBDD is the smallest in %u examples (%.2f%%)\n",zbddsmallest,100.0*zbddsmallest/POPULATION);
688  printf("TZBDD is the smallest in %u examples (%.2f%%)\n",tzbddsmallest,100.0*tzbddsmallest/POPULATION);
689  printf("OBDD and ZBDD are the same size and are smaller in %u examples (%.2f%%)\n",tzbddlargest,100.0*tzbddlargest/POPULATION);
690  printf("OBDD and TZBDD are the same size and are smaller in %u examples (%.2f%%)\n",zbddlargest,100.0*zbddlargest/POPULATION);
691  printf("ZBDD and TZBDD are the same size and are smaller in %u examples (%.2f%%)\n",obddlargest,100.0*obddlargest/POPULATION);
692  printf("all three graphs have the same size in %u examples (%.2f%%)\n",allsamesize,100.0*allsamesize/POPULATION);
693 
694  }
695 
696 }
697 
698 /* RESULTS */
699 /*
700 
701 RESULTS FOR POPULATION=10000, SIZE=8, RATIO=0.01
702 the average size of OBDDs = 16.83
703 the average size of ZBDDs = 10.33
704 the average size of TZBDDs = 10.31
705 OBDD is the smallest in 0 examples (0.00%)
706 ZBDD is the smallest in 188 examples (1.88%)
707 TZBDD is the smallest in 425 examples (4.25%)
708 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
709 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
710 ZBDD and TZBDD are the same size and are smaller in 9387 examples (93.87%)
711 all three graphs have the same size in 0 examples (0.00%)
712 
713 RESULTS FOR POPULATION=10000, SIZE=8, RATIO=0.10
714 the average size of OBDDs = 44.03
715 the average size of ZBDDs = 33.22
716 the average size of TZBDDs = 33.89
717 OBDD is the smallest in 0 examples (0.00%)
718 ZBDD is the smallest in 5425 examples (54.25%)
719 TZBDD is the smallest in 2154 examples (21.54%)
720 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
721 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
722 ZBDD and TZBDD are the same size and are smaller in 2421 examples (24.21%)
723 all three graphs have the same size in 0 examples (0.00%)
724 
725 RESULTS FOR POPULATION=10000, SIZE=8, RATIO=0.50
726 the average size of OBDDs = 63.79
727 the average size of ZBDDs = 60.68
728 the average size of TZBDDs = 66.23
729 OBDD is the smallest in 235 examples (2.35%)
730 ZBDD is the smallest in 8878 examples (88.78%)
731 TZBDD is the smallest in 26 examples (0.26%)
732 OBDD and ZBDD are the same size and are smaller in 835 examples (8.35%)
733 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
734 ZBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
735 all three graphs have the same size in 26 examples (0.26%)
736 
737 RESULTS FOR POPULATION=10000, SIZE=8, RATIO=0.90
738 the average size of OBDDs = 43.79
739 the average size of ZBDDs = 44.48
740 the average size of TZBDDs = 44.12
741 OBDD is the smallest in 1699 examples (16.99%)
742 ZBDD is the smallest in 2868 examples (28.68%)
743 TZBDD is the smallest in 0 examples (0.00%)
744 OBDD and ZBDD are the same size and are smaller in 693 examples (6.93%)
745 OBDD and TZBDD are the same size and are smaller in 3699 examples (36.99%)
746 ZBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
747 all three graphs have the same size in 1041 examples (10.41%)
748 
749 RESULTS FOR POPULATION=10000, SIZE=8, RATIO=0.99
750 the average size of OBDDs = 16.86
751 the average size of ZBDDs = 21.07
752 the average size of TZBDDs = 16.59
753 OBDD is the smallest in 0 examples (0.00%)
754 ZBDD is the smallest in 0 examples (0.00%)
755 TZBDD is the smallest in 2759 examples (27.59%)
756 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
757 OBDD and TZBDD are the same size and are smaller in 6947 examples (69.47%)
758 ZBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
759 all three graphs have the same size in 294 examples (2.94%)
760 
761 ---
762 
763 RESULTS FOR POPULATION=10000, SIZE=30, RATIO=1.00e-08
764 the average size of OBDDs = 262.92 (min = 233, max = 277)
765 the average size of ZBDDs = 136.48 (min = 113, max = 166)
766 the average size of TZBDDs = 136.48 (min = 113, max = 166)
767 OBDD is the smallest in 0 examples (0.00%)
768 ZBDD is the smallest in 0 examples (0.00%)
769 TZBDD is the smallest in 0 examples (0.00%)
770 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
771 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
772 ZBDD and TZBDD are the same size and are smaller in 10000 examples (100.00%)
773 all three graphs have the same size in 0 examples (0.00%)
774 
775 RESULTS FOR POPULATION=10000, SIZE=30, RATIO=1.00e-04
776 the average size of OBDDs = 181687.04 (min = 180434, max = 182742)
777 the average size of ZBDDs = 144380.62 (min = 143671, max = 145055)
778 the average size of TZBDDs = 144396.46 (min = 143694, max = 145070)
779 OBDD is the smallest in 0 examples (0.00%)
780 ZBDD is the smallest in 9681 examples (96.81%)
781 TZBDD is the smallest in 228 examples (2.28%)
782 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
783 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
784 ZBDD and TZBDD are the same size and are smaller in 91 examples (0.91%)
785 all three graphs have the same size in 0 examples (0.00%)
786 
787 RESULTS FOR POPULATION=10000, SIZE=30, RATIO=1.00e+00
788 the average size of OBDDs = 262.45 (min = 242, max = 277)
789 the average size of ZBDDs = 285.69 (min = 263, max = 302)
790 the average size of TZBDDs = 262.44 (min = 242, max = 277)
791 OBDD is the smallest in 0 examples (0.00%)
792 ZBDD is the smallest in 0 examples (0.00%)
793 TZBDD is the smallest in 50 examples (0.50%)
794 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
795 OBDD and TZBDD are the same size and are smaller in 9950 examples (99.50%)
796 ZBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
797 all three graphs have the same size in 0 examples (0.00%)
798 
799 ---
800 
801 RESULTS FOR POPULATION=1000, SIZE=63, RATIO=1.00e-16
802 the average size of OBDDs = 37237.49 (min = 36928, max = 37498)
803 the average size of ZBDDs = 19092.70 (min = 18774, max = 19394)
804 the average size of TZBDDs = 19092.70 (min = 18774, max = 19394)
805 OBDD is the smallest in 0 examples (0.00%)
806 ZBDD is the smallest in 0 examples (0.00%)
807 TZBDD is the smallest in 0 examples (0.00%)
808 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
809 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
810 ZBDD and TZBDD are the same size and are smaller in 1000 examples (100.00%)
811 all three graphs have the same size in 0 examples (0.00%)
812 
813 RESULTS FOR POPULATION=1000, SIZE=63, RATIO=1.00e+00
814 the average size of OBDDs = 41039.00 (min = 40743, max = 41381)
815 the average size of ZBDDs = 41088.37 (min = 40793, max = 41426)
816 the average size of TZBDDs = 41039.00 (min = 40743, max = 41381)
817 OBDD is the smallest in 0 examples (0.00%)
818 ZBDD is the smallest in 0 examples (0.00%)
819 TZBDD is the smallest in 0 examples (0.00%)
820 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
821 OBDD and TZBDD are the same size and are smaller in 1000 examples (100.00%)
822 ZBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
823 all three graphs have the same size in 0 examples (0.00%)
824 
825 */
#define Biddy_ResetVariablesValue()
Definition: biddy.h:460
#define Biddy_RandomSet(unit, r)
Definition: biddy.h:853
#define Biddy_SetVariableValue(v, f)
Definition: biddy.h:465
#define Biddy_ExistAbstract(f, cube)
Definition: biddy.h:783
unsigned long long int Biddy_Managed_CountPaths(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountPaths count the number of 1-paths.
Definition: biddyStat.c:1452
#define Biddy_E(f, v)
Definition: biddy.h:768
void * Biddy_Edge
Definition: biddy.h:262
#define Biddy_GetManagerType()
Definition: biddy.h:321
#define Biddy_And(f, g)
Definition: biddy.h:705
double Biddy_Managed_CountMinterms(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
Function Biddy_Managed_CountMinterms.
Definition: biddyStat.c:1520
Biddy_Variable Biddy_GetTopVariable(Biddy_Edge fun)
Function Biddy_GetTopVariable returns the top variable.
Definition: biddyMain.c:1285
Biddy_Edge Biddy_Managed_Copy(Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_Edge f)
Function Biddy_Managed_Copy copies a graph from one manager to another manager which can use the same...
Definition: biddyMain.c:5312
#define Biddy_DependentVariableNumber(f)
Definition: biddy.h:1054
#define Biddy_Change(f, v)
Definition: biddy.h:823
#define Biddy_CountPaths(f)
Definition: biddy.h:1064
#define Biddy_GetConstantOne()
Definition: biddy.h:393
#define Biddy_Restrict(f, v, value)
Definition: biddy.h:758
#define Biddy_Or(f, g)
Definition: biddy.h:713
void Biddy_ExitMNG(Biddy_Manager *mng)
Function Biddy_ExitMNG deletes a manager.
Definition: biddyMain.c:854
#define Biddy_AndAbstract(f, g, cube)
Definition: biddy.h:793
#define Biddy_GetBaseSet()
Definition: biddy.h:400
void ** Biddy_Manager
Definition: biddy.h:244
#define Biddy_Copy(MNG2, f)
Definition: biddy.h:666
#define Biddy_Xor(f, g)
Definition: biddy.h:730
unsigned int Biddy_Managed_WriteDot(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], int id, Biddy_Boolean cudd)
Function Biddy_Managed_WriteDot writes dot/graphviz format using fprintf.
Definition: biddyInOut.c:1111
#define Biddy_Leq(f, g)
Definition: biddy.h:740
Biddy_String Biddy_Managed_GetManagerName(Biddy_Manager MNG)
Function Biddy_Managed_GetManagerName reports the name of the BDD type used in the manager...
Definition: biddyMain.c:1126
unsigned short int Biddy_Variable
Definition: biddy.h:253
#define Biddy_Not(f)
Definition: biddy.h:694
void Biddy_InitMNG(Biddy_Manager *mng, int gddtype)
Function Biddy_InitMNG initialize a manager.
Definition: biddyMain.c:178
#define Biddy_GetConstantZero()
Definition: biddy.h:386
#define Biddy_CountMinterms(f, nvars)
Definition: biddy.h:1069
#define Biddy_Exit()
Definition: biddy.h:313
File biddy.h contains declaration of all external data structures.
#define Biddy_A(f, v)
Definition: biddy.h:773
Biddy_Edge Biddy_Managed_RandomFunction(Biddy_Manager MNG, Biddy_Edge support, double r)
Function Biddy_Managed_RandomFunction generates a random BDD.
Definition: biddyOp.c:5976
#define Biddy_CountNodesPlain(f)
Definition: biddy.h:1049
#define Biddy_DensityOfFunction(f, nvars)
Definition: biddy.h:1076
#define Biddy_ITE(f, g, h)
Definition: biddy.h:699
#define Biddy_GetVariableEdge(v)
Definition: biddy.h:430
unsigned int Biddy_Managed_DependentVariableNumber(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_DependentVariableNumber.
Definition: biddyStat.c:1275
#define Biddy_UnivAbstract(f, cube)
Definition: biddy.h:788
#define Biddy_CountNodes(f)
Definition: biddy.h:874
Biddy_Edge Biddy_Managed_And(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_And calculates Boolean function AND (conjunction).
#define Biddy_WriteDot(filename, f, label, id, cudd)
Definition: biddy.h:1160
#define Biddy_Gt(f, g)
Definition: biddy.h:745
unsigned int Biddy_Managed_CountNodes(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountNodes.
Definition: biddyStat.c:85
#define Biddy_GetManagerName()
Definition: biddy.h:326
unsigned int Biddy_Managed_CountNodesPlain(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountNodesPlain.
Definition: biddyStat.c:1191
#define Biddy_RandomFunction(support, r)
Definition: biddy.h:848
Biddy_Edge Biddy_Managed_GetConstantOne(Biddy_Manager MNG)
Function Biddy_Managed_GetConstantOne returns constant 1.
Definition: biddyMain.c:1586