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