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