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