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