Biddy  1.7.4
An academic Binary Decision Diagrams package
README.md
1 USER MANUAL
2 ==========
3 
4 ### TL;DR
5 --------------
6 
7 Biddy is a multi-platform academic Binary Decision Diagrams package.
8 It supports plain ROBDDs, ROBDDs with complemented edges,
9 0-sup-BDDs with complemented edges, and plain Tagged 0-sup-BDDs.
10 
11 Biddy is capable of all the typical operations regarding
12 Boolean functions, combination sets, and BDDs.
13 
14 Biddy is a library to be included in your C and C++ projects:
15 
16 ~~~
17 #include "/path/to/biddy.h"
18 ~~~
19 
20 To compile Biddy library use "make static" or "make dynamic" or "make debug".
21 There is no configuration script, you should edit Makefiles to adapt system
22 configuration.
23 
24 ~~~
25 biddy> make dynamic
26 biddy> make clean
27 ~~~
28 
29 Dependencies:
30 
31 - on GNU/Linux, you need libgmp (https://gmplib.org/).
32 - on MS Windows, you need MPIR library (http://mpir.org/).
33 
34 When using Biddy on GNU/Linux, you may have to tell bash about the library:
35 
36 ~~~
37 export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/absolute/path/to/biddy/library
38 ~~~
39 
40 There are two aditional packages included into Biddy distribution:
41 
42 - bddview is a pure Tcl/Tk script for visualization of BDDs,
43 - BDD Scout is a demo application demonstrating the capability of Biddy and bddview.
44 
45 Biddy is free software maintained by Robert Meolic
46 (robert.meolic@um.si) at University of Maribor, Slovenia.
47 
48 Homepage: http://biddy.meolic.com/
49 
50 ### 1. AN OVERVIEW
51 --------------
52 
53 Biddy supports ROBDDs as described in "K. S. Brace,
54 R. L. Rudell, R. E. Bryant. Efficient Implementation of a BDD
55 Package. 27th ACM/IEEE DAC, pages 40-45, 1990".
56 
57 Biddy supports 0-sup-BDDs as described in
58 "S. Minato. Zero-Suppressed BDDs for Set Manipulation in Combinatorial
59 Problems, 30th ACM/IEEE DAC, pages 272-277, 1993".
60 
61 Biddy supports Tagged 0-sup-BDDs (also denoted TZDDs or TZBDDs) as
62 introduced in "R. Meolic. Implementation aspects of a BDD package supporting
63 general decision diagrams, https://dk.um.si/IzpisGradiva.php?id=68831"
64 and described in "T. van Dijk, R. Wille, R. Meolic.
65 Tagged BDDs: Combining Reduction Rules from Different Decision Diagram Types,
66 17th FMCAD, pages 108-115, 2017".
67 
68 Biddy includes:
69 
70 - automatic garbage collection with a system age
71  (a variant of a mark-and-sweep approach),
72 - node management through formulae protecting,
73 - variable swapping and sifting algorithm for all supported BDD types.
74 
75 Biddy is optimized for efficiency, but it is mainly oriented towards
76 readable and comprehensible source code in C.
77 
78 Biddy is currently used in the following projects:
79 
80 - BDD Scout, demo project which allows visualization of BDDs and
81  also includes some benchmarks
82 - Efficient Symbolic Tools (EST), model checking and other algorithms
83  for formal verification of systems (http://est.meolic.com/)
84 
85 ### 2. SOURCE CODE
86 --------------
87 
88 Biddy is free software released under GPL.
89 
90 The short name of Biddy package is 'biddy'. This name is placed in front
91 of all filenames and external identifiers. It may appear in
92 all lowercase, or with its first letter capitalized, written as
93 'biddy' and 'Biddy', respectively.
94 
95 There are three categories of C functions.
96 
97 - Exported functions are visible outside the package.
98 - Internal functions are visible to all files within the package.
99 - Static functions are visible to the file only.
100 
101 There are two types of C functions.
102 
103 - General functions which operates on a particular BDD and considering only
104  graph properties (i.e. changing edge's mark, selecting nodes, counting nodes
105  etc.). These functions are the same for different type of decision diagrams
106  (BDD, ZDD, etc.). Functions, which add or delete nodes or those which needs
107  info about variables (e.g. a name or a value) are not general functions.
108  Exported general functions have prefix Biddy_.
109 - Managed functions, which operates on a global properties of a BDD system
110  (e.g. node table, variable table, formula table, various caches, etc.)
111  or consider a BDD as a Boolean function (e.g. Boolean operations, counting
112  minterms, etc.). These functions need info stored in a manager.
113  Exported managed functions have prefix Biddy_Managed_.
114 
115 Biddy consists of the following core files:
116 
117 - README.md (this file)
118 - CHANGES (history of changes)
119 - COPYING (license file)
120 - VERSION (project's version)
121 - Makefile (used to produce binary code)
122 - Makefile.Linux (Makefile definitions for GNU/Linux)
123 - Makefile.MINGW (Makefile definitions for MS Windows)
124 - Makefile.Darwin (Makefile definitions for MacOS)
125 - biddy.h (header)
126 - biddyInt.h (header)
127 - biddyMain.c (main functions)
128 - biddyOp.c (functions for operations on BDDs)
129 - biddyStat.c (functions for statistic)
130 - biddyInOut.c (parsers and generators for Boolean functions)
131 - package-source (script used to build distribution)
132 - package-bin (script used to build distribution)
133 - package-bin.bat (script used to build distribution)
134 - package-tgz (script used to build distribution)
135 - package-deb (script used to build distribution)
136 - package-rpm (script used to build distribution)
137 - debian/* (files used when creating deb package)
138 - rpm/* (files used when creating rpm package)
139 
140 There are two C headers, external and internal. The external header
141 file, named biddy.h, defines features visible from outside the
142 package. The internal header file, named biddyInt.h defines features
143 used in multiple files inside the package, but not outside.
144 
145 Details about building are given in Section 4.
146 
147 ### 3. USING BIDDY LIBRARY
148 ----------------------
149 
150 Precompiled packages include dynamically linked library
151 (i.e. *.so on GNU/Linux, *.dll on MS Windows, *.dylib on Mac OS X),
152 and the appropriate C header biddy.h. Currently, there are no interfaces
153 for other programming languages.
154 
155 For linking with Biddy library you have to use:
156 
157 ~~~
158 -lbiddy -lgmp
159 ~~~
160 
161 The following code is an example of usage.
162 Please note, that functions for node management are not shown. Moreover,
163 Biddy has a manager but its usage is optional and it is also not shown in
164 the given example.
165 
166 IMPORTANT:
167 You should define UNIX, MACOSX, or MINGW.
168 You should define USE_BIDDY iff you are using Biddy via dynamic library.
169 
170 ~~~
171 /* compile with gcc -o program.exe source.c -I. -L. -lbiddy -lgmp */
172 #define UNIX
173 #include "biddy.h"
174 
175 #define Str2Var(x) (Biddy_GetVariable((Biddy_String)x))
176 
177 int main() {
178  Biddy_Edge f,g,h,r;
179 
180  Biddy_Init(); /* use default, i.e. ROBDD WITH COMPLEMENTED EDGES */
181  printf("Biddy is using %s.\n",Biddy_GetManagerName());
182 
183  f = Biddy_Eval1((Biddy_String)"(OR H E L L O)"); /* PREFIX INPUT */
184  g = Biddy_Eval1((Biddy_String)"(AND W O R L D)"); /* PREFIX INPUT */
185  h = Biddy_Eval2((Biddy_String)"~(H * E * L * L)"); /* INFIX INPUT */
186 
187  /* BASIC OPERATION */
188  r = Biddy_Xor(f,g);
189 
190  /* REPLACE SOME VARIABLES */
191  Biddy_ResetVariablesValue();
192  Biddy_SetVariableValue(Str2Var("H"),Biddy_GetVariableEdge(Str2Var("L")));
193  Biddy_SetVariableValue(Str2Var("K"),Biddy_GetVariableEdge(Str2Var("L")));
194  Biddy_SetVariableValue(Str2Var("W"),Biddy_GetVariableEdge(Str2Var("L")));
195  r = Biddy_Replace(r);
196 
197  /* SIMPLE RESTRICTION */
198  r = Biddy_Restrict(r,Str2Var("E"),FALSE);
199 
200  /* COUDERT AND MADRE'S RESTRICT FUNCTION */
201  r = Biddy_Simplify(r,h);
202 
203  /* SOME STATS */
204  printf("Function r depends on %u variables.\n",Biddy_DependentVariableNumber(r));
205  printf("Function r has %.0f minterms.\n",Biddy_CountMinterms(r,0));
206  printf("BDD for function r has %u nodes.\n",Biddy_CountNodes(r));
207 
208  /* TRUTH TABLE */
209  printf("Here is a truth table for function r\n");
210  Biddy_PrintfTable(r);
211 
212  /* GRAPHVIZ/DOT OUTPUT */
213  Biddy_WriteDot("biddy.dot",r,"r",-1,FALSE);
214  printf("USE 'dot -y -Tpng -O biddy.dot' to visualize BDD for function r.\n");
215 
216  Biddy_Exit();
217 }
218 ~~~
219 
220 If you do not want to use the default BDD type you simply change the initialization
221 call. Supported BDD types are BIDDYTYPEOBDD, BIDDYTYPEOBDDC, BIDDYTYPEZBDDC, and
222 BIDDYTYPETZBDD.
223 
224 ~~~
225 Biddy_InitAnonymous(BIDDYTYPEZBDDC);
226 ~~~
227 
228 ### 3.1 NODE MANAGEMENT THROUGH FORMULAE PROTECTING
229 
230 Biddy includes powerful node management based on formulae tagging.
231 There are six user functions to maintain nodes.
232 
233 ### Biddy_AddFormula(name,bdd,c)
234 
235 Given BDD becomes a formula. Its nodes will be preserved for the given
236 number of cleanings. If (name != NULL) then formula is accessible by its
237 name. If formula with a given name already exists it is overwritten.
238 If (c == -1) then formula is refreshed but not preserved.
239 If (c == 0) then formula is persistently preserved. There are five
240 macros defined to simplify adding formulae: Biddy_AddTmpFormula(name,bdd),
241 Biddy_AddPersistentFormula(name,bdd), Biddy_KeepFormula(bdd),
242 Biddy_KeepFormulaUntilPurge(bdd), and Biddy_KeepFormulaProlonged(bdd,c).
243 
244 ### Biddy_DeleteFormula(name)
245 
246 Nodes of the given formula are marked as deleted.
247 Formula is not accessible by its name anymore.
248 Nodes of deleted formula which are preserved or persistently preserved
249 will not be removed by regular GC whilst Biddy_Purge will
250 immediately remove all of them.
251 
252 ### Biddy_Clean()
253 
254 Discard all nodes which were not preserved or which are not preserved
255 anymore. Obsolete nodes are not immediately removed, they will be removed
256 during the first garbage collection. Use Biddy_Purge or Biddy_PurgeAndReorder
257 to immediately remove all obsolete nodes.
258 
259 ### Biddy_Purge()
260 
261 Immediately removes all nodes which were not preserved or which are not
262 preserved anymore. Moreover, all formulae without a name are deleted!
263 All nodes from all deleted formulae are removed if they are not needed by
264 other formulae. Call to Biddy_Purge does not count as cleaning and thus all
265 preserved formulae remains preserved for the same number of cleanings.
266 
267 ### Biddy_PurgeAndReorder(bdd)
268 
269 The same as Biddy_Purge but also trigger reordering on function
270 (if BDD is given) or global reordering (if NULL is given).
271 
272 ### Biddy_Refresh(bdd)
273 
274 All obsolete nodes in the given bdd become fresh nodes. Formula is not
275 created and no information about the existing formulae is changed.
276 This function is needed to implement user's operation caches, only.
277 
278 ### 3.2. EXAMPLES OF NODE MANAGEMENT WITH BIDDY
279 
280 The first example is a straightforward calculation.
281 
282 ~~~
283 f1 = op(...);
284 f2 = op(...);
285 g1 = op(f1,f2,...);
286 Biddy_KeepFormula(g1); /* g1 is preserved for next cleaning */
287 f1 = op(...);
288 f2 = op(...);
289 g2 = op(f1,f2,...);
290 Biddy_KeepFormula(g2); /* g2 is preserved for next cleaning */
291 Biddy_Clean(); /* g1 and g2 are still usable, f1 and f2 are obsolete */
292 result = op(g1,g2,...);
293 Biddy_KeepFormulaUntilPurge(result); /* result is permanently preserved */
294 Biddy_Clean(); /* all nodes not belonging to result are immediately removed */
295 ~~~
296 
297 If additional garbage collection is needed also after the calculation of g1,
298 you can use the following code after the calculation of g1:
299 
300 ~~~
301 Biddy_KeepFormulaProlonged(g1,2); /* g1 is preserved for next two cleanings */
302 Biddy_Clean(); /* g1 remains preserved for next cleaning */
303 ~~~
304 
305 In this approach, f1 and f2 become obsolete after Biddy_Clean, but their
306 nodes are not immediately removed (automatic garbage collection is only
307 started when there are no free nodes in the system).
308 
309 Alternatively, you can use the following code which is simpler but somehow
310 less efficient because Biddy_Purge() always starts garbage collection:
311 
312 ~~~
313 f1 = op(...);
314 f2 = op(...);
315 g1 = op(f1,f2,...);
316 Biddy_AddTmpFormula("g1",g1); /* g1 is named */
317 Biddy_Purge(); /* keep only nodes from named formulae */
318 f1 = op(...);
319 f2 = op(...);
320 g2 = op(f1,f2,...);
321 Biddy_AddTmpFormula("g2",g2); /* g2 is named */
322 Biddy_Purge(); /* keep only nodes from named formulae */
323 result = op(g1,g2,...);
324 Biddy_AddPersistentFormula("result",result); /* result is permanently preserved */
325 Biddy_Clean(); /* tmp formulae becomes obsolete */
326 Biddy_Purge(); /* all nodes not belonging to result are immediately removed */
327 ~~~
328 
329 The second example is an iterative calculation:
330 
331 ~~~
332 result = op(...);
333 while (!finish) {
334  Biddy_KeepFormula(result); /* result is preserved for next cleaning */
335  Biddy_Clean(); /* result is still usable, f and g are obsolete */
336  f = op(...);
337  g = op(f,...);
338  result = op(result,g,...);
339 }
340 Biddy_KeepFormulaUntilPurge(result); /* result is permanently preserved */
341 Biddy_Clean(); /* tmp results are not needed, anymore */
342 ~~~
343 
344 If garbage collection is needed also after the calculation of g, you must
345 use the following code:
346 
347 ~~~
348 result = op(...);
349 while (!finish) {
350  Biddy_KeepFormulaProlonged(result,2); /* result is preserved for next two cleanings */
351  Biddy_Clean(); /* result remains preserved, f and g are obsolete */
352  f = op(...);
353  g = op(f,...);
354  Biddy_KeepFormula(g); /* g is preserved for next cleaning */
355  Biddy_Clean(); /* result and g are still usable, f is obsolete */
356  result = op(result,g,...);
357 }
358 Biddy_KeepFormulaUntilPurge(result); /* final result is permanently preserved */
359 Biddy_Clean(); /* tmp results are not needed, anymore */
360 ~~~
361 
362 The third example is an outline of an implementation of bisimulation:
363 
364 ~~~
365 init = AND(init_p,init_q)
366 Biddy_KeepFormulaUntilPurge(init) /* init is permanently preserved */
367 eq = InitialEq(init_p,tr_p,init_q,tr_q,...);
368 do {
369  Biddy_KeepFormula(eq); /* eq is preserved for next cleaning */
370  Biddy_Clean(); /* eq remains usable */
371  last = eq;
372  eq1 = NextEqPart1(eq,tr_p,tr_q,...);
373  eq2 = NextEqPart2(eq,tr_p,tr_q,...);
374  eq = AND(eq1,eq2);
375 } while (AND(init,eq)!=0 && eq!=last)
376 if (AND(init,eq)!=0) result=false; else result=true;
377 Biddy_Clean();
378 Biddy_Purge(); /* immediately remove all nodes created during the calculation */
379 ~~~
380 
381 The fourth example is an outline of an implementation of model checking where
382 we are trying to benefit from regularly reordering
383 (in contrast to Biddy_Purge(), Biddy_PurgeAndReorder() will delete named
384 tmp formulae):
385 
386 ~~~
387 sup = Prepare(...);
388 Biddy_AddPersistentFormula("sup",sup) /* sup is permanently preserved */
389 Z = 0;
390 last = 1;
391 while (Z!=last) {
392  Biddy_AddPersistentFormula("Z",Z); /* old Z is marked as deleted */
393  Biddy_PurgeAndReorder(Z); /* perform reordering to optimize Z */
394  last = Z;
395  Z = NextSet(Z,sup,...);
396 }
397 result = Z;
398 Biddy_AddPersistentFormula("result",result); /* final result is permanently preserved */
399 Biddy_DeleteFormula("sup"); /* sup is marked as deleted */
400 Biddy_DeleteFormula("Z"); /* Z is marked as deleted */
401 Biddy_Purge(); /* remove nodes not belonging to result */
402 ~~~
403 
404 The fifth example is an outline of an implementation of parallel composition
405 where we are trying to benefit from intensive GC:
406 
407 ~~~
408 sacc = snew = AND(init_1,init_2,...,init_N);
409 for (i=1;i<=N;i++) di[i] = 0;
410 for (i=1;i<=N;i++) for (j=1;i<=N;j++) dij[i,j] = 0;
411 do {
412  Biddy_KeepFormulaProlonged(snew,N*(N+1)); /* snew is preserved just long enough */
413  Biddy_KeepFormulaProlonged(sacc,N*(N+1)); /* sacc is preserved just long enough */
414  new1 = 0;
415  for (i=1;i<=N;i++) {
416  sup = OneStep(snew,tr_i,...);
417  di[i] = OR(d[i],sup);
418  new1 = OR(new1,NextState(sup,...));
419  Biddy_KeepFormulaProlonged(d[i],N*(N+1)); /* di[i] is preserved just long enough */
420  Biddy_KeepFormulaProlonged(new1,1); /* new1 is preserved for next cleaning, only */
421  Biddy_Clean(); /* new1 remains usable */
422  }
423  Biddy_KeepFormulaProlonged(new1,N*N); /* new1 is preserved just long enough */
424  new2 = 0;
425  for (i=1;i<=N;i++) for (j=1;j<=N;j++) {
426  sup = OneStep(snew,tr_i,tr_j,...);
427  dij[i,j] = OR(d[i,j],sup);
428  new2 = OR(new2,NextState(sup,...);
429  Biddy_KeepFormulaProlonged(dij[i,j],N*(N+1)); /* dij[i,j] is preserved just long enough */
430  Biddy_KeepFormulaProlonged(new2,1); /* new2 is preserved for next cleaning, only */
431  Biddy_Clean(); /* new2 remains usable */
432  }
433  snew = AND(OR(new1,new2),NOT(sacc));
434  sacc = OR(sacc,snew);
435 } while (snew!=0)
436 tr1 = 0;
437 for (i=1;i<=N;i++) {
438  sup = AddStab(di[i],...);
439  tr1 = OR(tr1,sup);
440  Biddy_KeepFormulaProlonged(tr1,1); /* tr1 is preserved for next cleaning, only */
441  Biddy_Clean(); /* tr1 remains usable */
442 }
443 Biddy_KeepFormulaProlonged(tr1,N*N); /* tr1 is preserved just long enough */
444 tr2 = 0;
445 for (i=1;i<=N;i++) for (j=1;j<=N;j++) {
446  sup = AddStab(dij[i,j],...);
447  tr2 = OR(tr2,sup);
448  Biddy_KeepFormulaProlonged(tr2,1); /* tr2 is preserved for next cleaning, only */
449  Biddy_Clean(); /* tr2 remains usable */
450 }
451 result = OR(tr1,tr2);
452 Biddy_KeepFormulaUntilPurge(result); /* final result is permanently preserved */
453 Biddy_Clean(); /* tmp results are not needed, anymore */
454 ~~~
455 
456 ### 3.3 MORE DETAILS ON MEMORY MANAGEMENT (SYSTEM AGE AND NODE CHAINING)
457 
458 Garbage collection is automatically triggered if nodes from all reserved
459 blocks of nodes are used. Garbage collection will remove as many
460 obsolete nodes as possible.
461 
462 Biddy does not use reference counter but a different approach.
463 We call the implemented algorithm "GC with a system age".
464 It is a variant of a mark-and-sweep approach.
465 
466 Using system age instead of reference counter has
467 some advantages. It allows GC to be started in any time
468 without breaking the ongoing calculation. Thus, there is no need
469 to taking care of repeating broken calculations. Moreover,
470 the usage of system age instead of reference counter
471 removes all the hassle of referencing and dereferencing nodes
472 and thus it is favorable in an academic package oriented towards
473 simple and readable source code.
474 
475 There are four classes of nodes. Every node belongs to one of
476 these classes:
477 
478 - __fortified__ node (expiry value == 0);
479 - __fresh__ node (expiry value == biddySystemAge);
480 - __prolonged__ node (expiry value > biddySystemAge);
481 - __obsolete__ node (0 < expiry value < biddySystemAge).
482 
483 Before each GC, nodes must be refreshed in such a way that no successor of
484 a non-obsolete node is obsolete. This is achieved with a relatively simple
485 loop which check every nodes at most once.
486 
487 Biddy relies on a single hash table for all variables. However, it supports
488 chaining of nodes to form different lists (using an extra pointer in
489 each node). This facility is used to improve efficiency of garbage
490 collection and sifting.
491 
492 Please node, that node chaining is not determined or limited by
493 using formulae protecting schema or a system age approach, it is
494 an independent mechanism.
495 
496 ### 4. BUILDING PACKAGES
497 --------------------
498 
499 ### Compiling Biddy library
500 
501 On GNU/Linux, we are using gcc.
502 
503 ~~~
504 biddy> make dynamic
505 biddy> make clean
506 ~~~
507 
508 Alternatively, you can use:
509 
510 ~~~
511 biddy> make static
512 biddy> make debug
513 biddy> make profile
514 ~~~
515 
516 You can use specify the target folder:
517 
518 ~~~
519 biddy> make dynamic "BINDIR = ./bin"
520 biddy> make clean "BINDIR = ./bin"
521 ~~~
522 
523 On MS Windows, we are using MSYS2.
524 We use pacman to prepare the environment:
525 
526 ~~~
527 MSYS shell> pacman -Syuu
528 MSYS shell> pacman -S mingw-w64-i686-gcc
529 MSYS shell> pacman -S mingw-w64-x86_64-gcc
530 MSYS shell> pacman -S make
531 MSYS shell> pacman -S bison
532 MSYS shell> pacman -S gdb
533 MSYS shell> pacman -S nano
534 MSYS shell> pacman -S tar
535 MSYS shell> pacman -S subversion
536 ~~~
537 
538 Alternatively, you can use Visual Studio for building.
539 There is a prepared solution consisting of many projects.
540 You need to adapt include and lib folders.
541 
542 ~~~
543 ./VS/Biddy.sln
544 ~~~
545 
546 To produce nice setup files, we use Advanced Installer
547 (http://www.advancedinstaller.com/).
548 We have been granted a free licence. MANY THANKS!
549 
550 ### Dependencies
551 
552 On GNU/Linux, we are using libgmp (https://gmplib.org/).
553 
554 On MS Windows, we are using MPIR library (http://mpir.org/).
555 
556 ### Creating Biddy library as a zip package
557 
558 ~~~
559 biddy> ./package-bin
560 ~~~
561 
562 You need a zip program.
563 
564 On MS Windows, you need 7-Zip (http://7-zip.org/) - and it has a strange
565 use of -x! You also need file 7zsd_All_x64.sfx that you should
566 download as part of "7z SFX Tools" from http://7zsfx.info/en/ and put
567 in the directory containing 7z.exe.
568 
569 You install the resulting package by extracting libraries to the
570 appropriate directory (may be local, e.g. user's home directory).
571 
572 When using this package on GNU/Linux, you have to tell bash about the library:
573 
574 ~~~
575 export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/absolute/path/to/biddy/library
576 ~~~
577 
578 ### Creating zip file with source code of a complete Biddy project
579 
580 ~~~
581 biddy> ./package-source
582 ~~~
583 
584 If available, source code of bddview and BDD Scout will be included, too.
585 
586 ### Creating packages for GNU/Linux
587 
588 ~~~
589 biddy> ./package-tgz
590 biddy> ./package-deb
591 biddy> ./package-rpm
592 ~~~
593 
594 These scripts are intedend to be used on Ubuntu.
595 These scripts needs release number as an argument. Script package-tgz
596 must be invoked before running package-deb. Debian packages must be
597 created before RPM packages.
598 
599 ./package-tgz should create orig.tar.gz file and prepare directories
600 for creating debian and RPM packages. You can run ./package-tgz only
601 if version changes.
602 
603 ./package-deb should create debian packages (libbidy and
604 libbiddy-dev). They are tested on Ubuntu system.
605 
606 ./package-rpm should create RPM packages (libbidy and libbiddy-devel).
607 They are tested on openSUSE system.
608 
609 ### Creating demo aplication bddscout
610 
611 You need complete sources for biddy, bddview, and bddscout,
612 Scripts are located in biddy/bddscout.
613 
614 ~~~
615 bddscout> ./package-bin
616 bddscout> ./package-tgz
617 bddscout> ./package-deb
618 bddscout> ./package-rpm
619 ~~~
620 
621 package-bin should create BDD Scout (staticaly linked with Biddy
622 library). The script will produce a zip file. You install BDD Scout
623 by simply unzip to the target directory.
624 
625 ./package-tgz should create orig.tar.gz file and prepare directories
626 for creating debian and RPM packages. You can run ./package-tgz only
627 if version changes.
628 
629 ./package-deb should create debian packages (bddscout, bddscout-bra,
630 bddscout-ifip, bddscout-bddtrace, bddscout-ifip-data, and
631 bddscout-bddtrace-data). They are tested on Ubuntu system.
632 
633 ./package-rpm should create RPM packages (bddscout, bddscout-bra,
634 bddscout-ifip, bddscout-bddtrace, bddscout-ifip-data, and
635 bddscout-bddtrace-data). They are tested on openSUSE system.
636 
637 ### 5. HISTORY
638 ----------
639 
640 Biddy is based on a BDD package written in Pascal in 1992 as a student
641 project. At that time, it was a great work and the paper about it won
642 a second place at IEEE Region Student Paper Contest (Paris-Evry,
643 1993). The paper was published by IEEE as "A. Casar, R. Meolic.
644 Representation of Boolean functions with ROBDDs. IEEE Student paper
645 contest : regional contest winners 1990-1997 : prize-winning papers
646 demonstrating student excellence worldwide, Piscataway, 2000" and can
647 be obtained from http://research.meolic.com/papers/robdd.pdf
648 
649 In 1995, this BDD package was rewritten in C. Later, this BDD package
650 become an integral part of EST package, a prototype tool for formal
651 verification of concurrent systems. The homepage for EST project is
652 http://est.meolic.com/
653 
654 In 2003, BDD package from EST was included in the report presented at
655 16th Symposium on Integrated Circuits and Systems Design (SBCCI'03).
656 The report is available as a paper "G. Janssen. A Consumer Report on
657 BDD Packages. IBM T.J. Watson Research Center. 2003". Get it from
658 http://doi.ieeecomputersociety.org/10.1109/SBCCI.2003.1232832
659 
660 In 2006, BDD package in EST got the name Biddy.
661 
662 In 2007, a main part of Biddy package was extracted from EST forming a
663 separate package called Biddy. The code has been reorganized in such a
664 way, that EST is not using internal structures (e.g. node table)
665 directly but using the provided API only.
666 
667 In 2007, we created local svn repository for maintaining the source
668 code (not live, anymore).
669 
670 On May 15, 2008, Biddy v1.0 was released containing also bddview
671 v0.95 (Tcl/Tk BDD viewer) and Bdd Scout v0.90 (demo application).
672 
673 In 2009, 2010, and 2012 updated versions of Biddy v1.0 were released
674 which added support for debian packaging, support for RPM packaging,
675 fix errors, and improve documentation, packaging, and Tcl/Tk GUI.
676 
677 In 2012, a research paper about Biddy library appears in
678 Journal of Software (doi:10.4304/jsw.7.6.1358-1366)
679 http://ojs.academypublisher.com/index.php/jsw/article/view/jsw070613581366/
680 
681 In 2013, Biddy v1.1 was released. Biddy_Edge became a pointer instead
682 of structure and all other structures were optimized.
683 
684 In 2014, Biddy v1.2 was released. Variable swapping and sifting algorithm
685 were the most significant additions.
686 
687 In 2014, svn repositories for biddy, bddview and bddscout are moved
688 to Savannah. http://svn.savannah.nongnu.org/viewvc/?root=biddy
689 
690 In 2015, Biddy v1.3, v.1.4 and v1.5 was released. Various input/output methods
691 have been added. Support for 64-bit arhitectures and support for Visual Studio
692 projects were improved. Biddy got a manager. Many CUDD-like functions have been
693 added. Comment's style changed to support doxygen. HTML and PDF documentation
694 were produced.
695 
696 Also in 2015, Personal Package Archive ppa:meolic/biddy has been created
697 https://launchpad.net/~meolic/+archive/ubuntu/biddy
698 
699 Also in 2015, sources became available on GitHub
700 https://github.com/meolic/biddy
701 
702 In 2016, Biddy v1.6 was released. Formulae are not recursively refreshed
703 all the time, anymore. The size of Node table became resizable.
704 
705 In 2017, Biddy v1.7 was released (there were 4 minor releases, the
706 last one was Biddy v1.7.4). Terminology has changed a lot,
707 e.g. "formulae counter" became "system age". Added support for ROBDDs
708 without complemented edges, 0-sup-BDDs and Tagged 0-sup-BDDs. Implemented
709 creation and manipulaton of non-anonymous managers. Added manipulation of
710 combination sets. Improved many functionalities, e.g sifting.
711 Many new CUDD-like functions have been added.
712 Moreover, bddview and BDD Scout have been significantly improved.
713 
714 ### 6. PUBLICATIONS
715 ---------------
716 
717 If you find our work useful, please, cite us.
718 
719 - Robert Meolic. __Biddy - a multi-platform academic BDD package.__
720  Journal of Software, 7(6), pp. 1358-1366, 2012.
721  http://ojs.academypublisher.com/index.php/jsw/article/view/jsw070613581366
722 
723 - Robert Meolic. __Implementation aspects of a BDD package supporting general decision diagrams.__
724  Technical report, University of Maribor, 2016.
725  https://dk.um.si/IzpisGradiva.php?id=68831
726 
727 - Robert Meolic. __Biddy.__
728  We are preparing a paper for SCP.