Biddy  1.7.1
An academic Binary Decision Diagrams package
biddy-example-random.c
1 /* $Revision: 244 $ */
2 /* $Date: 2017-02-14 23:23:32 +0100 (tor, 14 feb 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 -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 #define POPULATION -1
20 #define SIZE 4
21 #define RATIO 0.5
22 
23 /* create Boolean function (BOOLEANFUNCTION) or combination set (COMBINATIONSET) */
24 #define RANDOMTYPE BOOLEANFUNCTION
25 #define BDDTYPE BIDDYTYPEOBDD
26 
27 int main() {
28  Biddy_Manager MNGOBDD,MNGZBDD,MNGTZBDD;
29  Biddy_Edge tmp,support,cube,result,result0,result1,result2;
30  Biddy_Edge robdd,rzbdd,rtzbdd;
31  Biddy_Variable v,first,last,extra;
32  unsigned int i;
33  unsigned int s1,s2,s3;
34 
35  unsigned int obddsize,zbddsize,tzbddsize;
36  unsigned int obddminsize,zbddminsize,tzbddminsize;
37  unsigned int obddmaxsize,zbddmaxsize,tzbddmaxsize;
38  unsigned int obddsmallest,zbddsmallest,tzbddsmallest;
39  unsigned int obddlargest,zbddlargest,tzbddlargest;
40  unsigned int allsamesize;
41 
42  if (POPULATION == -1) {
43 
44  Biddy_InitAnonymous(BDDTYPE);
45 
46  Biddy_InitMNG(&MNGOBDD,BIDDYTYPEOBDD);
47  Biddy_InitMNG(&MNGZBDD,BIDDYTYPEZBDD);
48  Biddy_InitMNG(&MNGTZBDD,BIDDYTYPETZBDD);
49 
50 /* for OBDDs, support is the most easiest calculated using AddVariable and AND */
51 #if (BDDTYPE == BIDDYTYPEOBDD)
52  printf("Using OBDDs...\n");
53  tmp = Biddy_AddVariable();
54  support = tmp;
55  first = Biddy_GetTopVariable(tmp);
56  for (v=1; v<SIZE; v++) {
57  tmp = Biddy_AddVariable();
58  support = Biddy_And(support,tmp);
59  }
60  last = Biddy_GetTopVariable(tmp);
61  tmp = Biddy_AddVariable();
62  extra = Biddy_GetTopVariable(tmp);
63 #endif
64 
65 /* for ZBDDs, support is the most easiest calculated using AddElement and CHANGE */
66 #if (BDDTYPE == BIDDYTYPEZBDD)
67  printf("Using ZBDDs...\n");
68  tmp = Biddy_AddElement();
69  support = tmp;
70  first = Biddy_GetTopVariable(tmp);
71  for (v=1; v<SIZE; v++) {
72  tmp = Biddy_AddElement();
73  support = Biddy_Change(support,Biddy_GetTopVariable(tmp));
74  }
75  last = Biddy_GetTopVariable(tmp);
76  tmp = Biddy_AddElement();
77  extra = Biddy_GetTopVariable(tmp);
78 #endif
79 
80 /* for TZBDDs, the approaches from OBDDs and ZBDDs are both working, using the first one */
81 #if (BDDTYPE == BIDDYTYPETZBDD)
82  printf("Using TZBDDs...\n");
83  tmp = Biddy_AddVariable();
84  support = tmp;
85  first = Biddy_GetTopVariable(tmp);
86  for (v=1; v<SIZE; v++) {
87  tmp = Biddy_AddVariable();
88  support = Biddy_And(support,tmp);
89  }
90  last = Biddy_GetTopVariable(tmp);
91  tmp = Biddy_AddVariable();
92  extra = Biddy_GetTopVariable(tmp);
93 #endif
94 
95  /* GRAPHVIZ/DOT OUTPUT OF support - DEBUGGING, ONLY */
96  /*
97  if (SIZE < 10) {
98  Biddy_WriteDot("support.dot",support,"support",-1,FALSE);
99  printf("USE 'dot -y -Tpng -O support.dot' to visualize function support.\n");
100  }
101  */
102 
103  result = NULL;
104 
105 #if (RANDOMTYPE == BOOLEANFUNCTION)
106  printf("Generating random Boolean function...\n");
107  result = Biddy_Random(support,RATIO);
108 #endif
109 
110 #if (RANDOMTYPE == COMBINATIONSET)
111  printf("Generating random combination set...\n");
112  result = Biddy_RandomSet(support,RATIO);
113 #endif
114 
115  if (result == NULL) {
116  printf("ERROR: Function result is NULL!\n");
117  exit(1);
118  }
119 
120  /* GRAPHVIZ/DOT OUTPUT OF THE RESULT - DEBUGGING, ONLY */
121  /*
122  if (SIZE < 10) {
123  printf("HERE IS A TRUTH TABLE FOR result:\n");
124  Biddy_PrintfTable(result);
125  Biddy_WriteDot("result.dot",result,"result",-1,FALSE);
126  printf("USE 'dot -y -Tpng -O result.dot' to visualize function result.\n");
127  }
128  */
129 
130  printf("Function result has %.0f minterms/combinations.\n",Biddy_CountMinterm(result,SIZE));
131  printf("Function result has density = %.2e.\n",Biddy_DensityFunction(result,SIZE));
132 
133  /* *** BEGINNING OF TESTING OPERATIONS *** */
134 
135  /* OPERATION SUBSET */
136 
137  result0 = Biddy_Subset0(result,first);
138  result1 = Biddy_Subset1(result,first);
139 
140  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
141  /*
142  if (SIZE < 10) {
143  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
144  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
145  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
146  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
147  }
148  */
149 
150  printf("Function result has %.0f minterms/combinations where first variable/element is NEGATIVE/ABSENT.\n",Biddy_CountMinterm(result0,SIZE));
151  printf("Function result has %.0f minterms/combinations where first variable/element is POSITIVE/PRESENT.\n",Biddy_CountMinterm(result1,SIZE));
152 
153  s1 = (unsigned int) Biddy_CountMinterm(result,SIZE);
154  s2 = (unsigned int) Biddy_CountMinterm(result0,SIZE);
155  s3 = (unsigned int) Biddy_CountMinterm(result1,SIZE);
156 
157  if (s1 != (s2 + s3)) {
158  printf("ERROR: Operation Subset is wrong!\n");
159  }
160 
161  result0 = Biddy_Subset0(result,last);
162  result1 = Biddy_Subset1(result,last);
163 
164  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
165  /*
166  if (SIZE < 10) {
167  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
168  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
169  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
170  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
171  }
172  */
173 
174  printf("Function result has %.0f minterms/combinations where last variable/element is NEGATIVE/ABSENT.\n",Biddy_CountMinterm(result0,SIZE));
175  printf("Function result has %.0f minterms/combinations where last variable/element is POSITIVE/PRESENT.\n",Biddy_CountMinterm(result1,SIZE));
176 
177  s1 = (unsigned int) Biddy_CountMinterm(result,SIZE);
178  s2 = (unsigned int) Biddy_CountMinterm(result0,SIZE);
179  s3 = (unsigned int) Biddy_CountMinterm(result1,SIZE);
180 
181  if (s1 != (s2 + s3)) {
182  printf("ERROR: Operation Subset is wrong!\n");
183  }
184 
185  /* OPERATION RESTRICT */
186 
187  result0 = Biddy_Restrict(result,first,FALSE);
188  result1 = Biddy_Restrict(result,first,TRUE);
189 
190  printf("If first variable is restricted to FALSE, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result0,SIZE));
191  printf("If first variable is restricted to TRUE, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result1,SIZE));
192 
193  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
194  /*
195  if (SIZE < 10) {
196  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
197  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
198  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
199  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
200  }
201  */
202 
203  s1 = (unsigned int) Biddy_CountMinterm(result,SIZE);
204  s2 = (unsigned int) Biddy_CountMinterm(result0,SIZE);
205  s3 = (unsigned int) Biddy_CountMinterm(result1,SIZE);
206 
207  if ((s1 + s1) != (s2 + s3)) {
208  printf("ERROR: Operation Restrict is wrong!\n");
209  }
210 
211  result0 = Biddy_Restrict(result,last,FALSE);
212  result1 = Biddy_Restrict(result,last,TRUE);
213 
214  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
215  /*
216  if (SIZE < 10) {
217  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
218  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
219  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
220  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
221  }
222  */
223 
224  printf("If last variable is restricted to FALSE, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result0,SIZE));
225  printf("If last variable is restricted to TRUE, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result1,SIZE));
226 
227  s1 = (unsigned int) Biddy_CountMinterm(result,SIZE);
228  s2 = (unsigned int) Biddy_CountMinterm(result0,SIZE);
229  s3 = (unsigned int) Biddy_CountMinterm(result1,SIZE);
230 
231  if ((s1 + s1) != (s2 + s3)) {
232  printf("ERROR: Operation Restrict is wrong!\n");
233  }
234 
235  /* OPERATION REPLACE */
236 
239 
240  result0 = Biddy_Replace(result);
241 
244 
245  result1 = Biddy_Replace(result0);
246 
247  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
248  /*
249  if (SIZE < 10) {
250  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
251  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
252  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
253  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
254  }
255  */
256 
257  if (result1 != result) {
258  printf("ERROR: Operation Replace is wrong!\n");
259  }
260 
261  /* OPERATION QUANTIFICATION */
262 
263  result0 = Biddy_E(result,first);
264  result1 = Biddy_A(result,first);
265 
266  printf("After the existential quantification of first variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result0,SIZE));
267  printf("After the universal quantification of first variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result1,SIZE));
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  s1 = (unsigned int) Biddy_CountMinterm(result,SIZE);
280  s2 = (unsigned int) Biddy_CountMinterm(result0,SIZE);
281  s3 = (unsigned int) Biddy_CountMinterm(result1,SIZE);
282 
283  if ((s1 + s1) != (s2 + s3)) {
284  printf("ERROR: Operation Quantification is wrong!\n");
285  }
286 
287  result0 = Biddy_E(result,last);
288  result1 = Biddy_A(result,last);
289 
290  /* GRAPHVIZ/DOT OUTPUT OF RESULT0 AND RESULT1 - DEBUGGING, ONLY */
291  /*
292  if (SIZE < 10) {
293  Biddy_WriteDot("result0.dot",result0,"result0",-1,FALSE);
294  printf("USE 'dot -y -Tpng -O result0.dot' to visualize function result0.\n");
295  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
296  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
297  }
298  */
299 
300  printf("After the existential quantification of last variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result0,SIZE));
301  printf("After the universal quantification of last variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result1,SIZE));
302 
303  s1 = (unsigned int) Biddy_CountMinterm(result,SIZE);
304  s2 = (unsigned int) Biddy_CountMinterm(result0,SIZE);
305  s3 = (unsigned int) Biddy_CountMinterm(result1,SIZE);
306 
307  if ((s1 + s1) != (s2 + s3)) {
308  printf("ERROR: Operation Quantification is wrong!\n");
309  }
310 
311  /* OPERATION ABSTRACTION */
312 
313  /* calculate cube */
314 
315 #if (BDDTYPE == BIDDYTYPEOBDD)
316  cube = Biddy_GetConstantOne();
317  cube = Biddy_And(cube,Biddy_GetVariableEdge(first));
318  cube = Biddy_And(cube,Biddy_GetVariableEdge(last));
319  cube = Biddy_And(cube,Biddy_GetVariableEdge(extra));
320 #endif
321 
322 #if (BDDTYPE == BIDDYTYPEZBDD)
323  cube = Biddy_GetBaseSet();
324  cube = Biddy_Change(cube,first);
325  cube = Biddy_Change(cube,last);
326  cube = Biddy_Change(cube,extra);
327 #endif
328 
329 #if (BDDTYPE == BIDDYTYPETZBDD)
330  cube = Biddy_GetConstantOne();
331  cube = Biddy_And(cube,Biddy_GetVariableEdge(first));
332  cube = Biddy_And(cube,Biddy_GetVariableEdge(last));
333  cube = Biddy_And(cube,Biddy_GetVariableEdge(extra));
334 #endif
335 
336  result1 = Biddy_E(result,first);
337  result1 = Biddy_E(result1,last);
338  result2 = Biddy_ExistAbstract(result,cube);
339 
340  printf("After the existential abstraction of first and last variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result2,SIZE));
341 
342  /* GRAPHVIZ/DOT OUTPUT OF RESULT1 - DEBUGGING, ONLY */
343  /*
344  if (SIZE < 10) {
345  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
346  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
347  }
348  */
349 
350  if (result1 != result2) {
351  printf("ERROR: Operation Abstraction is wrong!\n");
352  }
353 
354  result1 = Biddy_A(result,first);
355  result1 = Biddy_A(result1,last);
356  result2 = Biddy_UnivAbstract(result,cube);
357 
358  printf("After the universal abstraction of first and last variable, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result2,SIZE));
359 
360  /* GRAPHVIZ/DOT OUTPUT OF RESULT1 - DEBUGGING, ONLY */
361  /*
362  if (SIZE < 10) {
363  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
364  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
365  }
366  */
367 
368  if (result1 != result2) {
369  printf("ERROR: Operation Abstraction is wrong!\n");
370  }
371 
372  result0 = Biddy_E(result,first);
373  result1 = Biddy_E(Biddy_Not(result),last);
374  result2 = Biddy_And(result0,result1);
375  result2 = Biddy_ExistAbstract(result2,cube);
376  result1 = Biddy_AndAbstract(result0,result1,cube);
377 
378  printf("After the first user-defined abstraction, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result1,SIZE));
379 
380  if (result1 != result2) {
381  printf("ERROR: Operation Abstraction is wrong!\n");
382  }
383 
384  result0 = Biddy_A(result,first);
385  result1 = Biddy_A(Biddy_Not(result),last);
386  result1 = Biddy_AndAbstract(result0,result1,cube);
387 
388  printf("After the second user-defined abstraction, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result1,SIZE));
389 
390  if (result1 != Biddy_GetConstantZero()) {
391  printf("ERROR: Operation Abstraction is wrong!\n");
392  }
393 
394  /* BOOLEAN OPERATIONS AND OPERATION ITE */
395 
396  result1 = Biddy_ITE(Biddy_E(result,first),Biddy_E(result,last),Biddy_A(result,last));
397  result2 = Biddy_ITE(Biddy_A(result,first),Biddy_E(result,last),Biddy_A(result,last));
398 
399  printf("After the first ITE, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result1,SIZE));
400  printf("After the second ITE, function result has %.0f minterms/combinations\n",Biddy_CountMinterm(result2,SIZE));
401 
402  /* GRAPHVIZ/DOT OUTPUT OF RESULT1 AND RESULT2 - DEBUGGING, ONLY */
403  /*
404  if (SIZE < 10) {
405  Biddy_WriteDot("result1.dot",result1,"result1",-1,FALSE);
406  printf("USE 'dot -y -Tpng -O result1.dot' to visualize function result1.\n");
407  Biddy_WriteDot("result2.dot",result2,"result2",-1,FALSE);
408  printf("USE 'dot -y -Tpng -O result2.dot' to visualize function result2.\n");
409  }
410  */
411 
412  if (result1 != Biddy_Xor(
413  Biddy_And(Biddy_E(result,first),Biddy_E(result,last)),
414  Biddy_And(Biddy_Not(Biddy_E(result,first)),Biddy_A(result,last))))
415  {
416  printf("ERROR: result1 for Boolean operations ITE-AND-XOR-NOT is wrong!\n");
417  }
418  if (result1 != Biddy_Or(
419  Biddy_And(Biddy_E(result,first),Biddy_E(result,last)),
420  Biddy_Gt(Biddy_A(result,last),Biddy_E(result,first))))
421  {
422  printf("ERROR: result1 for Boolean operations ITE-AND-OR-GT is wrong!\n");
423  }
424 
425  if (result2 != Biddy_Xor(
426  Biddy_And(Biddy_A(result,first),Biddy_E(result,last)),
427  Biddy_And(Biddy_Not(Biddy_A(result,first)),Biddy_A(result,last))))
428  {
429  printf("ERROR: result2 for Boolean operations ITE-AND-XOR-NOT is wrong!\n");
430  }
431  if (result2 != Biddy_Or(
432  Biddy_And(Biddy_A(result,first),Biddy_E(result,last)),
433  Biddy_Gt(Biddy_A(result,last),Biddy_A(result,first))))
434  {
435  printf("ERROR: result2 for Boolean operations ITE-AND-OR-GT is wrong!\n");
436  }
437 
438  /* *** END OF TESTING OPERATIONS *** */
439 
440  /* CONVERT THE RESULT INTO OBDDs */
441  robdd = Biddy_Copy(MNGOBDD,result);
442  printf("OBDD for function result has %u nodes.\n",Biddy_Managed_NodeNumber(MNGOBDD,robdd));
443  printf("OBDD without complemented edges for function result has %u nodes (including both constants).\n",Biddy_Managed_NodeNumberPlain(MNGOBDD,robdd));
444  printf("OBDD for function result has %llu one-paths.\n",Biddy_Managed_CountPaths(MNGOBDD,robdd));
445  printf("OBDD for function result has %.0f minterms/combinations.\n",Biddy_Managed_CountMinterm(MNGOBDD,robdd,SIZE));
446  /* GRAPHVIZ/DOT OUTPUT OF THE RESULT */
447  if (SIZE < 10) {
448  Biddy_Managed_WriteDot(MNGOBDD,"obdd.dot",robdd,"obdd",-1,FALSE);
449  printf("USE 'dot -y -Tpng -O obdd.dot' to visualize OBDD for function result.\n");
450  }
451 
452  /* CONVERT THE RESULT INTO ZBDDs */
453  if (Biddy_GetManagerType() != BIDDYTYPETZBDD) {
454  rzbdd = Biddy_Copy(MNGZBDD,result);
455  printf("ZBDD for function result has %u nodes.\n",Biddy_Managed_NodeNumber(MNGZBDD,rzbdd));
456  printf("ZBDD without complemented edges for function result has %u nodes (including both constants).\n",Biddy_Managed_NodeNumberPlain(MNGZBDD,rzbdd));
457  printf("ZBDD for function result has %llu one-paths.\n",Biddy_Managed_CountPaths(MNGZBDD,rzbdd));
458  printf("ZBDD for function result has %.0f minterms/combinations.\n",Biddy_Managed_CountMinterm(MNGZBDD,rzbdd,SIZE));
459  /* GRAPHVIZ/DOT OUTPUT OF THE RESULT */
460  if (SIZE < 10) {
461  Biddy_Managed_WriteDot(MNGZBDD,"zbdd.dot",rzbdd,"zbdd",-1,FALSE);
462  printf("USE 'dot -y -Tpng -O zbdd.dot' to visualize ZBDD for function result.\n");
463  }
464  }
465 
466  if (Biddy_GetManagerType() != BIDDYTYPEZBDD) {
467  /* CONVERT THE RESULT INTO TZBDDs */
468  rtzbdd = Biddy_Copy(MNGTZBDD,result);
469  printf("TZBDD for function result has %u nodes.\n",Biddy_Managed_NodeNumber(MNGTZBDD,rtzbdd));
470  printf("TZBDD for function result has %llu one-paths.\n",Biddy_Managed_CountPaths(MNGTZBDD,rtzbdd));
471  printf("TZBDD for function result has %.0f minterms/combinations.\n",Biddy_Managed_CountMinterm(MNGTZBDD,rtzbdd,SIZE));
472  /* GRAPHVIZ/DOT OUTPUT OF THE RESULT */
473  if (SIZE < 10) {
474  Biddy_Managed_WriteDot(MNGTZBDD,"tzbdd.dot",rtzbdd,"tzbdd",-1,FALSE);
475  printf("USE 'dot -y -Tpng -O tzbdd.dot' to visualize TZBDD for function result.\n");
476  }
477  }
478 
479  Biddy_Exit();
480  Biddy_ExitMNG(&MNGOBDD);
481  Biddy_ExitMNG(&MNGZBDD);
482  Biddy_ExitMNG(&MNGTZBDD);
483 
484  } else {
485 
486  obddsize = zbddsize = tzbddsize = 0;
487  obddminsize = zbddminsize = tzbddminsize = 0;
488  obddmaxsize = zbddmaxsize = tzbddmaxsize = 0;
489  obddsmallest = zbddsmallest = tzbddsmallest = 0;
490  obddlargest = zbddlargest = tzbddlargest = 0;
491  allsamesize = 0;
492 
493  for (i=0; i<POPULATION; i++) {
494 
495  Biddy_InitMNG(&MNGOBDD,BIDDYTYPEOBDD);
496  Biddy_InitMNG(&MNGZBDD,BIDDYTYPEZBDD);
497  Biddy_InitMNG(&MNGTZBDD,BIDDYTYPETZBDD);
498 
499  support = Biddy_Managed_GetConstantOne(MNGOBDD);
500  for (v=0; v<SIZE; v++) {
501  support = Biddy_Managed_And(MNGOBDD,support,Biddy_Managed_AddVariable(MNGOBDD));
502  }
503 
504  robdd = Biddy_Managed_Random(MNGOBDD,support,RATIO);
505  rzbdd = Biddy_Managed_Copy(MNGOBDD,MNGZBDD,robdd);
506  rtzbdd = Biddy_Managed_Copy(MNGOBDD,MNGTZBDD,robdd);
507 
508  s1 = Biddy_Managed_NodeNumber(MNGOBDD,robdd);
509  s2 = Biddy_Managed_NodeNumber(MNGZBDD,rzbdd);
510  s3 = Biddy_Managed_NodeNumber(MNGTZBDD,rtzbdd);
511 
512  obddsize += s1;
513  zbddsize += s2;
514  tzbddsize += s3;
515 
516  if (obddminsize == 0) obddminsize = s1;
517  if (zbddminsize == 0) zbddminsize = s2;
518  if (tzbddminsize == 0) tzbddminsize = s3;
519 
520  if (s1 < obddminsize) obddminsize = s1;
521  if (s2 < zbddminsize) zbddminsize = s2;
522  if (s3 < tzbddminsize) tzbddminsize = s3;
523 
524  if (s1 > obddmaxsize) obddmaxsize = s1;
525  if (s2 > zbddmaxsize) zbddmaxsize = s2;
526  if (s3 > tzbddmaxsize) tzbddmaxsize = s3;
527 
528  if ((s1 < s2) && (s1 < s3)) obddsmallest++;
529  if ((s2 < s1) && (s2 < s3)) zbddsmallest++;
530  if ((s3 < s1) && (s3 < s2)) tzbddsmallest++;
531  if ((s1 == s2) && (s1 < s3)) tzbddlargest++;
532  if ((s1 == s3) && (s1 < s2)) zbddlargest++;
533  if ((s2 == s3) && (s2 < s1)) obddlargest++;
534  if ((s1 == s2) && (s2 == s3)) allsamesize++;
535 
536  Biddy_ExitMNG(&MNGOBDD);
537  Biddy_ExitMNG(&MNGZBDD);
538  Biddy_ExitMNG(&MNGTZBDD);
539 
540  }
541 
542  printf("RESULTS FOR POPULATION=%u, SIZE=%u, RATIO=%.2e\n",POPULATION,SIZE,RATIO);
543  printf("the average size of OBDDs = %.2f (min = %u, max = %u)\n",1.0*obddsize/POPULATION,obddminsize,obddmaxsize);
544  printf("the average size of ZBDDs = %.2f (min = %u, max = %u)\n",1.0*zbddsize/POPULATION,zbddminsize,zbddmaxsize);
545  printf("the average size of TZBDDs = %.2f (min = %u, max = %u)\n",1.0*tzbddsize/POPULATION,tzbddminsize,tzbddmaxsize);
546  printf("OBDD is the smallest in %u examples (%.2f%%)\n",obddsmallest,100.0*obddsmallest/POPULATION);
547  printf("ZBDD is the smallest in %u examples (%.2f%%)\n",zbddsmallest,100.0*zbddsmallest/POPULATION);
548  printf("TZBDD is the smallest in %u examples (%.2f%%)\n",tzbddsmallest,100.0*tzbddsmallest/POPULATION);
549  printf("OBDD and ZBDD are the same size and are smaller in %u examples (%.2f%%)\n",tzbddlargest,100.0*tzbddlargest/POPULATION);
550  printf("OBDD and TZBDD are the same size and are smaller in %u examples (%.2f%%)\n",zbddlargest,100.0*zbddlargest/POPULATION);
551  printf("ZBDD and TZBDD are the same size and are smaller in %u examples (%.2f%%)\n",obddlargest,100.0*obddlargest/POPULATION);
552  printf("all three graphs have the same size in %u examples (%.2f%%)\n",allsamesize,100.0*allsamesize/POPULATION);
553 
554  }
555 
556 }
557 
558 /* RESULTS */
559 /*
560 
561 RESULTS FOR POPULATION=10000, SIZE=8, RATIO=0.01
562 the average size of OBDDs = 16.83
563 the average size of ZBDDs = 10.33
564 the average size of TZBDDs = 10.31
565 OBDD is the smallest in 0 examples (0.00%)
566 ZBDD is the smallest in 188 examples (1.88%)
567 TZBDD is the smallest in 425 examples (4.25%)
568 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
569 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
570 ZBDD and TZBDD are the same size and are smaller in 9387 examples (93.87%)
571 all three graphs have the same size in 0 examples (0.00%)
572 
573 RESULTS FOR POPULATION=10000, SIZE=8, RATIO=0.10
574 the average size of OBDDs = 44.03
575 the average size of ZBDDs = 33.22
576 the average size of TZBDDs = 33.89
577 OBDD is the smallest in 0 examples (0.00%)
578 ZBDD is the smallest in 5425 examples (54.25%)
579 TZBDD is the smallest in 2154 examples (21.54%)
580 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
581 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
582 ZBDD and TZBDD are the same size and are smaller in 2421 examples (24.21%)
583 all three graphs have the same size in 0 examples (0.00%)
584 
585 RESULTS FOR POPULATION=10000, SIZE=8, RATIO=0.50
586 the average size of OBDDs = 63.79
587 the average size of ZBDDs = 60.68
588 the average size of TZBDDs = 66.23
589 OBDD is the smallest in 235 examples (2.35%)
590 ZBDD is the smallest in 8878 examples (88.78%)
591 TZBDD is the smallest in 26 examples (0.26%)
592 OBDD and ZBDD are the same size and are smaller in 835 examples (8.35%)
593 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
594 ZBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
595 all three graphs have the same size in 26 examples (0.26%)
596 
597 RESULTS FOR POPULATION=10000, SIZE=8, RATIO=0.90
598 the average size of OBDDs = 43.79
599 the average size of ZBDDs = 44.48
600 the average size of TZBDDs = 44.12
601 OBDD is the smallest in 1699 examples (16.99%)
602 ZBDD is the smallest in 2868 examples (28.68%)
603 TZBDD is the smallest in 0 examples (0.00%)
604 OBDD and ZBDD are the same size and are smaller in 693 examples (6.93%)
605 OBDD and TZBDD are the same size and are smaller in 3699 examples (36.99%)
606 ZBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
607 all three graphs have the same size in 1041 examples (10.41%)
608 
609 RESULTS FOR POPULATION=10000, SIZE=8, RATIO=0.99
610 the average size of OBDDs = 16.86
611 the average size of ZBDDs = 21.07
612 the average size of TZBDDs = 16.59
613 OBDD is the smallest in 0 examples (0.00%)
614 ZBDD is the smallest in 0 examples (0.00%)
615 TZBDD is the smallest in 2759 examples (27.59%)
616 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
617 OBDD and TZBDD are the same size and are smaller in 6947 examples (69.47%)
618 ZBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
619 all three graphs have the same size in 294 examples (2.94%)
620 
621 ---
622 
623 RESULTS FOR POPULATION=10000, SIZE=30, RATIO=1.00e-08
624 the average size of OBDDs = 262.92 (min = 233, max = 277)
625 the average size of ZBDDs = 136.48 (min = 113, max = 166)
626 the average size of TZBDDs = 136.48 (min = 113, max = 166)
627 OBDD is the smallest in 0 examples (0.00%)
628 ZBDD is the smallest in 0 examples (0.00%)
629 TZBDD is the smallest in 0 examples (0.00%)
630 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
631 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
632 ZBDD and TZBDD are the same size and are smaller in 10000 examples (100.00%)
633 all three graphs have the same size in 0 examples (0.00%)
634 
635 RESULTS FOR POPULATION=10000, SIZE=30, RATIO=1.00e-04
636 the average size of OBDDs = 181687.04 (min = 180434, max = 182742)
637 the average size of ZBDDs = 144380.62 (min = 143671, max = 145055)
638 the average size of TZBDDs = 144396.46 (min = 143694, max = 145070)
639 OBDD is the smallest in 0 examples (0.00%)
640 ZBDD is the smallest in 9681 examples (96.81%)
641 TZBDD is the smallest in 228 examples (2.28%)
642 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
643 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
644 ZBDD and TZBDD are the same size and are smaller in 91 examples (0.91%)
645 all three graphs have the same size in 0 examples (0.00%)
646 
647 RESULTS FOR POPULATION=10000, SIZE=30, RATIO=1.00e+00
648 the average size of OBDDs = 262.45 (min = 242, max = 277)
649 the average size of ZBDDs = 285.69 (min = 263, max = 302)
650 the average size of TZBDDs = 262.44 (min = 242, max = 277)
651 OBDD is the smallest in 0 examples (0.00%)
652 ZBDD is the smallest in 0 examples (0.00%)
653 TZBDD is the smallest in 50 examples (0.50%)
654 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
655 OBDD and TZBDD are the same size and are smaller in 9950 examples (99.50%)
656 ZBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
657 all three graphs have the same size in 0 examples (0.00%)
658 
659 ---
660 
661 RESULTS FOR POPULATION=1000, SIZE=63, RATIO=1.00e-16
662 the average size of OBDDs = 37237.49 (min = 36928, max = 37498)
663 the average size of ZBDDs = 19092.70 (min = 18774, max = 19394)
664 the average size of TZBDDs = 19092.70 (min = 18774, max = 19394)
665 OBDD is the smallest in 0 examples (0.00%)
666 ZBDD is the smallest in 0 examples (0.00%)
667 TZBDD is the smallest in 0 examples (0.00%)
668 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
669 OBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
670 ZBDD and TZBDD are the same size and are smaller in 1000 examples (100.00%)
671 all three graphs have the same size in 0 examples (0.00%)
672 
673 RESULTS FOR POPULATION=1000, SIZE=63, RATIO=1.00e+00
674 the average size of OBDDs = 41039.00 (min = 40743, max = 41381)
675 the average size of ZBDDs = 41088.37 (min = 40793, max = 41426)
676 the average size of TZBDDs = 41039.00 (min = 40743, max = 41381)
677 OBDD is the smallest in 0 examples (0.00%)
678 ZBDD is the smallest in 0 examples (0.00%)
679 TZBDD is the smallest in 0 examples (0.00%)
680 OBDD and ZBDD are the same size and are smaller in 0 examples (0.00%)
681 OBDD and TZBDD are the same size and are smaller in 1000 examples (100.00%)
682 ZBDD and TZBDD are the same size and are smaller in 0 examples (0.00%)
683 all three graphs have the same size in 0 examples (0.00%)
684 
685 */
Biddy_Edge Biddy_Managed_And(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_And calculates Boolean function AND (conjunction).
Definition: biddyMain.c:2699
#define Biddy_ResetVariablesValue()
Definition: biddy.h:404
#define Biddy_CountMinterm(f, nvars)
Definition: biddy.h:905
#define Biddy_RandomSet(unit, r)
Definition: biddy.h:714
#define Biddy_SetVariableValue(v, f)
Definition: biddy.h:409
#define Biddy_ExistAbstract(f, cube)
Definition: biddy.h:556
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:1151
#define Biddy_E(f, v)
Definition: biddy.h:541
void * Biddy_Edge
Definition: biddy.h:221
#define Biddy_GetManagerType()
Definition: biddy.h:280
#define Biddy_And(f, g)
Definition: biddy.h:478
unsigned int Biddy_Managed_NodeNumberPlain(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_NodeNumberPlain.
Definition: biddyStat.c:976
Biddy_Edge Biddy_Managed_Random(Biddy_Manager MNG, Biddy_Edge support, double r)
Function Biddy_Managed_Random generates a random BDD.
Definition: biddyMain.c:6918
#define Biddy_Random(support, r)
Definition: biddy.h:709
Biddy_Variable Biddy_GetTopVariable(Biddy_Edge fun)
Function Biddy_GetTopVariable returns the top variable.
Definition: biddyMain.c:1060
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. DescriptionThe functi...
Definition: biddyMain.c:6766
#define Biddy_Change(f, v)
Definition: biddy.h:592
#define Biddy_GetConstantOne()
Definition: biddy.h:347
#define Biddy_Restrict(f, v, value)
Definition: biddy.h:531
#define Biddy_Or(f, g)
Definition: biddy.h:486
void Biddy_ExitMNG(Biddy_Manager *mng)
Function Biddy_ExitMNG deletes a manager.
Definition: biddyMain.c:691
#define Biddy_AndAbstract(f, g, cube)
Definition: biddy.h:566
#define Biddy_GetBaseSet()
Definition: biddy.h:354
void ** Biddy_Manager
Definition: biddy.h:203
#define Biddy_DensityFunction(f, nvars)
Definition: biddy.h:912
#define Biddy_Copy(MNG2, f)
Definition: biddy.h:694
#define Biddy_Xor(f, g)
Definition: biddy.h:503
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:914
unsigned short int Biddy_Variable
Definition: biddy.h:212
#define Biddy_Not(f)
Definition: biddy.h:467
unsigned int Biddy_Managed_NodeNumber(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_NodeNumber.
Definition: biddyStat.c:85
void Biddy_InitMNG(Biddy_Manager *mng, int gddtype)
Function Biddy_InitMNG initialize a manager.
Definition: biddyMain.c:210
#define Biddy_GetConstantZero()
Definition: biddy.h:340
#define Biddy_Exit()
Definition: biddy.h:272
File biddy.h contains declaration of all external data structures.
#define Biddy_Replace(f)
Definition: biddy.h:587
#define Biddy_A(f, v)
Definition: biddy.h:546
#define Biddy_ITE(f, g, h)
Definition: biddy.h:472
#define Biddy_GetVariableEdge(v)
Definition: biddy.h:374
#define Biddy_UnivAbstract(f, cube)
Definition: biddy.h:561
double Biddy_Managed_CountMinterm(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
Function Biddy_Managed_CountMinterm.
Definition: biddyStat.c:1202
#define Biddy_Gt(f, g)
Definition: biddy.h:518
Biddy_Edge Biddy_Managed_GetConstantOne(Biddy_Manager MNG)
Function Biddy_Managed_GetConstantOne returns constant 1.
Definition: biddyMain.c:1349