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