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