Biddy  1.7.4
An academic Binary Decision Diagrams package
USER MANUAL

### TL;DR

Biddy is a multi-platform academic Binary Decision Diagrams package. It supports plain ROBDDs, ROBDDs with complemented edges, 0-sup-BDDs with complemented edges, and plain Tagged 0-sup-BDDs.

Biddy is capable of all the typical operations regarding Boolean functions, combination sets, and BDDs.

Biddy is a library to be included in your C and C++ projects:

1 #include "/path/to/biddy.h"

To compile Biddy library use "make static" or "make dynamic" or "make debug". There is no configuration script, you should edit Makefiles to adapt system configuration.

1 biddy> make dynamic
2 biddy> make clean

Dependencies:

When using Biddy on GNU/Linux, you may have to tell bash about the library:

1 export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/absolute/path/to/biddy/library

There are two aditional packages included into Biddy distribution:

  • bddview is a pure Tcl/Tk script for visualization of BDDs,
  • BDD Scout is a demo application demonstrating the capability of Biddy and bddview.

Biddy is free software maintained by Robert Meolic (rober.nosp@m.t.me.nosp@m.olic@.nosp@m.um.s.nosp@m.i) at University of Maribor, Slovenia.

Homepage: http://biddy.meolic.com/

### 1. AN OVERVIEW

Biddy supports ROBDDs as described in "K. S. Brace, R. L. Rudell, R. E. Bryant. Efficient Implementation of a BDD Package. 27th ACM/IEEE DAC, pages 40-45, 1990".

Biddy supports 0-sup-BDDs as described in "S. Minato. Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems, 30th ACM/IEEE DAC, pages 272-277, 1993".

Biddy supports Tagged 0-sup-BDDs (also denoted TZDDs or TZBDDs) as introduced in "R. Meolic. Implementation aspects of a BDD package supporting general decision diagrams, https://dk.um.si/IzpisGradiva.php?id=68831" and described in "T. van Dijk, R. Wille, R. Meolic. Tagged BDDs: Combining Reduction Rules from Different Decision Diagram Types, 17th FMCAD, pages 108-115, 2017".

Biddy includes:

  • automatic garbage collection with a system age (a variant of a mark-and-sweep approach),
  • node management through formulae protecting,
  • variable swapping and sifting algorithm for all supported BDD types.

Biddy is optimized for efficiency, but it is mainly oriented towards readable and comprehensible source code in C.

Biddy is currently used in the following projects:

  • BDD Scout, demo project which allows visualization of BDDs and also includes some benchmarks
  • Efficient Symbolic Tools (EST), model checking and other algorithms for formal verification of systems (http://est.meolic.com/)

### 2. SOURCE CODE

Biddy is free software released under GPL.

The short name of Biddy package is 'biddy'. This name is placed in front of all filenames and external identifiers. It may appear in all lowercase, or with its first letter capitalized, written as 'biddy' and 'Biddy', respectively.

There are three categories of C functions.

  • Exported functions are visible outside the package.
  • Internal functions are visible to all files within the package.
  • Static functions are visible to the file only.

There are two types of C functions.

  • General functions which operates on a particular BDD and considering only graph properties (i.e. changing edge's mark, selecting nodes, counting nodes etc.). These functions are the same for different type of decision diagrams (BDD, ZDD, etc.). Functions, which add or delete nodes or those which needs info about variables (e.g. a name or a value) are not general functions. Exported general functions have prefix Biddy_.
  • Managed functions, which operates on a global properties of a BDD system (e.g. node table, variable table, formula table, various caches, etc.) or consider a BDD as a Boolean function (e.g. Boolean operations, counting minterms, etc.). These functions need info stored in a manager. Exported managed functions have prefix Biddy_Managed_.

Biddy consists of the following core files:

  • README.md (this file)
  • CHANGES (history of changes)
  • COPYING (license file)
  • VERSION (project's version)
  • Makefile (used to produce binary code)
  • Makefile.Linux (Makefile definitions for GNU/Linux)
  • Makefile.MINGW (Makefile definitions for MS Windows)
  • Makefile.Darwin (Makefile definitions for MacOS)
  • biddy.h (header)
  • biddyInt.h (header)
  • biddyMain.c (main functions)
  • biddyOp.c (functions for operations on BDDs)
  • biddyStat.c (functions for statistic)
  • biddyInOut.c (parsers and generators for Boolean functions)
  • package-source (script used to build distribution)
  • package-bin (script used to build distribution)
  • package-bin.bat (script used to build distribution)
  • package-tgz (script used to build distribution)
  • package-deb (script used to build distribution)
  • package-rpm (script used to build distribution)
  • debian/* (files used when creating deb package)
  • rpm/* (files used when creating rpm package)

There are two C headers, external and internal. The external header file, named biddy.h, defines features visible from outside the package. The internal header file, named biddyInt.h defines features used in multiple files inside the package, but not outside.

Details about building are given in Section 4.

### 3. USING BIDDY LIBRARY

Precompiled packages include dynamically linked library (i.e. *.so on GNU/Linux, *.dll on MS Windows, *.dylib on Mac OS X), and the appropriate C header biddy.h. Currently, there are no interfaces for other programming languages.

For linking with Biddy library you have to use:

1 -lbiddy -lgmp

The following code is an example of usage. Please note, that functions for node management are not shown. Moreover, Biddy has a manager but its usage is optional and it is also not shown in the given example.

IMPORTANT: You should define UNIX, MACOSX, or MINGW. You should define USE_BIDDY iff you are using Biddy via dynamic library.

1 /* compile with gcc -o program.exe source.c -I. -L. -lbiddy -lgmp */
2 #define UNIX
3 #include "biddy.h"
4 
5 #define Str2Var(x) (Biddy_GetVariable((Biddy_String)x))
6 
7 int main() {
8  Biddy_Edge f,g,h,r;
9 
10  Biddy_Init(); /* use default, i.e. ROBDD WITH COMPLEMENTED EDGES */
11  printf("Biddy is using %s.\n",Biddy_GetManagerName());
12 
13  f = Biddy_Eval1((Biddy_String)"(OR H E L L O)"); /* PREFIX INPUT */
14  g = Biddy_Eval1((Biddy_String)"(AND W O R L D)"); /* PREFIX INPUT */
15  h = Biddy_Eval2((Biddy_String)"~(H * E * L * L)"); /* INFIX INPUT */
16 
17  /* BASIC OPERATION */
18  r = Biddy_Xor(f,g);
19 
20  /* REPLACE SOME VARIABLES */
21  Biddy_ResetVariablesValue();
22  Biddy_SetVariableValue(Str2Var("H"),Biddy_GetVariableEdge(Str2Var("L")));
23  Biddy_SetVariableValue(Str2Var("K"),Biddy_GetVariableEdge(Str2Var("L")));
24  Biddy_SetVariableValue(Str2Var("W"),Biddy_GetVariableEdge(Str2Var("L")));
25  r = Biddy_Replace(r);
26 
27  /* SIMPLE RESTRICTION */
28  r = Biddy_Restrict(r,Str2Var("E"),FALSE);
29 
30  /* COUDERT AND MADRE'S RESTRICT FUNCTION */
31  r = Biddy_Simplify(r,h);
32 
33  /* SOME STATS */
34  printf("Function r depends on %u variables.\n",Biddy_DependentVariableNumber(r));
35  printf("Function r has %.0f minterms.\n",Biddy_CountMinterms(r,0));
36  printf("BDD for function r has %u nodes.\n",Biddy_CountNodes(r));
37 
38  /* TRUTH TABLE */
39  printf("Here is a truth table for function r\n");
40  Biddy_PrintfTable(r);
41 
42  /* GRAPHVIZ/DOT OUTPUT */
43  Biddy_WriteDot("biddy.dot",r,"r",-1,FALSE);
44  printf("USE 'dot -y -Tpng -O biddy.dot' to visualize BDD for function r.\n");
45 
46  Biddy_Exit();
47 }

If you do not want to use the default BDD type you simply change the initialization call. Supported BDD types are BIDDYTYPEOBDD, BIDDYTYPEOBDDC, BIDDYTYPEZBDDC, and BIDDYTYPETZBDD.

1 Biddy_InitAnonymous(BIDDYTYPEZBDDC);

3.1 NODE MANAGEMENT THROUGH FORMULAE PROTECTING

Biddy includes powerful node management based on formulae tagging. There are six user functions to maintain nodes.

Biddy_AddFormula(name,bdd,c)

Given BDD becomes a formula. Its nodes will be preserved for the given number of cleanings. If (name != NULL) then formula is accessible by its name. If formula with a given name already exists it is overwritten. If (c == -1) then formula is refreshed but not preserved. If (c == 0) then formula is persistently preserved. There are five macros defined to simplify adding formulae: Biddy_AddTmpFormula(name,bdd), Biddy_AddPersistentFormula(name,bdd), Biddy_KeepFormula(bdd), Biddy_KeepFormulaUntilPurge(bdd), and Biddy_KeepFormulaProlonged(bdd,c).

Biddy_DeleteFormula(name)

Nodes of the given formula are marked as deleted. Formula is not accessible by its name anymore. Nodes of deleted formula which are preserved or persistently preserved will not be removed by regular GC whilst Biddy_Purge will immediately remove all of them.

Biddy_Clean()

Discard all nodes which were not preserved or which are not preserved anymore. Obsolete nodes are not immediately removed, they will be removed during the first garbage collection. Use Biddy_Purge or Biddy_PurgeAndReorder to immediately remove all obsolete nodes.

Biddy_Purge()

Immediately removes all nodes which were not preserved or which are not preserved anymore. Moreover, all formulae without a name are deleted! All nodes from all deleted formulae are removed if they are not needed by other formulae. Call to Biddy_Purge does not count as cleaning and thus all preserved formulae remains preserved for the same number of cleanings.

Biddy_PurgeAndReorder(bdd)

The same as Biddy_Purge but also trigger reordering on function (if BDD is given) or global reordering (if NULL is given).

Biddy_Refresh(bdd)

All obsolete nodes in the given bdd become fresh nodes. Formula is not created and no information about the existing formulae is changed. This function is needed to implement user's operation caches, only.

3.2. EXAMPLES OF NODE MANAGEMENT WITH BIDDY

The first example is a straightforward calculation.

1 f1 = op(...);
2 f2 = op(...);
3 g1 = op(f1,f2,...);
4 Biddy_KeepFormula(g1); /* g1 is preserved for next cleaning */
5 f1 = op(...);
6 f2 = op(...);
7 g2 = op(f1,f2,...);
8 Biddy_KeepFormula(g2); /* g2 is preserved for next cleaning */
9 Biddy_Clean(); /* g1 and g2 are still usable, f1 and f2 are obsolete */
10 result = op(g1,g2,...);
11 Biddy_KeepFormulaUntilPurge(result); /* result is permanently preserved */
12 Biddy_Clean(); /* all nodes not belonging to result are immediately removed */

If additional garbage collection is needed also after the calculation of g1, you can use the following code after the calculation of g1:

1 Biddy_KeepFormulaProlonged(g1,2); /* g1 is preserved for next two cleanings */
2 Biddy_Clean(); /* g1 remains preserved for next cleaning */

In this approach, f1 and f2 become obsolete after Biddy_Clean, but their nodes are not immediately removed (automatic garbage collection is only started when there are no free nodes in the system).

Alternatively, you can use the following code which is simpler but somehow less efficient because Biddy_Purge() always starts garbage collection:

1 f1 = op(...);
2 f2 = op(...);
3 g1 = op(f1,f2,...);
4 Biddy_AddTmpFormula("g1",g1); /* g1 is named */
5 Biddy_Purge(); /* keep only nodes from named formulae */
6 f1 = op(...);
7 f2 = op(...);
8 g2 = op(f1,f2,...);
9 Biddy_AddTmpFormula("g2",g2); /* g2 is named */
10 Biddy_Purge(); /* keep only nodes from named formulae */
11 result = op(g1,g2,...);
12 Biddy_AddPersistentFormula("result",result); /* result is permanently preserved */
13 Biddy_Clean(); /* tmp formulae becomes obsolete */
14 Biddy_Purge(); /* all nodes not belonging to result are immediately removed */

The second example is an iterative calculation:

1 result = op(...);
2 while (!finish) {
3  Biddy_KeepFormula(result); /* result is preserved for next cleaning */
4  Biddy_Clean(); /* result is still usable, f and g are obsolete */
5  f = op(...);
6  g = op(f,...);
7  result = op(result,g,...);
8 }
9 Biddy_KeepFormulaUntilPurge(result); /* result is permanently preserved */
10 Biddy_Clean(); /* tmp results are not needed, anymore */

If garbage collection is needed also after the calculation of g, you must use the following code:

1 result = op(...);
2 while (!finish) {
3  Biddy_KeepFormulaProlonged(result,2); /* result is preserved for next two cleanings */
4  Biddy_Clean(); /* result remains preserved, f and g are obsolete */
5  f = op(...);
6  g = op(f,...);
7  Biddy_KeepFormula(g); /* g is preserved for next cleaning */
8  Biddy_Clean(); /* result and g are still usable, f is obsolete */
9  result = op(result,g,...);
10 }
11 Biddy_KeepFormulaUntilPurge(result); /* final result is permanently preserved */
12 Biddy_Clean(); /* tmp results are not needed, anymore */

The third example is an outline of an implementation of bisimulation:

1 init = AND(init_p,init_q)
2 Biddy_KeepFormulaUntilPurge(init) /* init is permanently preserved */
3 eq = InitialEq(init_p,tr_p,init_q,tr_q,...);
4 do {
5  Biddy_KeepFormula(eq); /* eq is preserved for next cleaning */
6  Biddy_Clean(); /* eq remains usable */
7  last = eq;
8  eq1 = NextEqPart1(eq,tr_p,tr_q,...);
9  eq2 = NextEqPart2(eq,tr_p,tr_q,...);
10  eq = AND(eq1,eq2);
11 } while (AND(init,eq)!=0 && eq!=last)
12 if (AND(init,eq)!=0) result=false; else result=true;
13 Biddy_Clean();
14 Biddy_Purge(); /* immediately remove all nodes created during the calculation */

The fourth example is an outline of an implementation of model checking where we are trying to benefit from regularly reordering (in contrast to Biddy_Purge(), Biddy_PurgeAndReorder() will delete named tmp formulae):

1 sup = Prepare(...);
2 Biddy_AddPersistentFormula("sup",sup) /* sup is permanently preserved */
3 Z = 0;
4 last = 1;
5 while (Z!=last) {
6  Biddy_AddPersistentFormula("Z",Z); /* old Z is marked as deleted */
7  Biddy_PurgeAndReorder(Z); /* perform reordering to optimize Z */
8  last = Z;
9  Z = NextSet(Z,sup,...);
10 }
11 result = Z;
12 Biddy_AddPersistentFormula("result",result); /* final result is permanently preserved */
13 Biddy_DeleteFormula("sup"); /* sup is marked as deleted */
14 Biddy_DeleteFormula("Z"); /* Z is marked as deleted */
15 Biddy_Purge(); /* remove nodes not belonging to result */

The fifth example is an outline of an implementation of parallel composition where we are trying to benefit from intensive GC:

1 sacc = snew = AND(init_1,init_2,...,init_N);
2 for (i=1;i<=N;i++) di[i] = 0;
3 for (i=1;i<=N;i++) for (j=1;i<=N;j++) dij[i,j] = 0;
4 do {
5  Biddy_KeepFormulaProlonged(snew,N*(N+1)); /* snew is preserved just long enough */
6  Biddy_KeepFormulaProlonged(sacc,N*(N+1)); /* sacc is preserved just long enough */
7  new1 = 0;
8  for (i=1;i<=N;i++) {
9  sup = OneStep(snew,tr_i,...);
10  di[i] = OR(d[i],sup);
11  new1 = OR(new1,NextState(sup,...));
12  Biddy_KeepFormulaProlonged(d[i],N*(N+1)); /* di[i] is preserved just long enough */
13  Biddy_KeepFormulaProlonged(new1,1); /* new1 is preserved for next cleaning, only */
14  Biddy_Clean(); /* new1 remains usable */
15  }
16  Biddy_KeepFormulaProlonged(new1,N*N); /* new1 is preserved just long enough */
17  new2 = 0;
18  for (i=1;i<=N;i++) for (j=1;j<=N;j++) {
19  sup = OneStep(snew,tr_i,tr_j,...);
20  dij[i,j] = OR(d[i,j],sup);
21  new2 = OR(new2,NextState(sup,...);
22  Biddy_KeepFormulaProlonged(dij[i,j],N*(N+1)); /* dij[i,j] is preserved just long enough */
23  Biddy_KeepFormulaProlonged(new2,1); /* new2 is preserved for next cleaning, only */
24  Biddy_Clean(); /* new2 remains usable */
25  }
26  snew = AND(OR(new1,new2),NOT(sacc));
27  sacc = OR(sacc,snew);
28 } while (snew!=0)
29 tr1 = 0;
30 for (i=1;i<=N;i++) {
31  sup = AddStab(di[i],...);
32  tr1 = OR(tr1,sup);
33  Biddy_KeepFormulaProlonged(tr1,1); /* tr1 is preserved for next cleaning, only */
34  Biddy_Clean(); /* tr1 remains usable */
35 }
36 Biddy_KeepFormulaProlonged(tr1,N*N); /* tr1 is preserved just long enough */
37 tr2 = 0;
38 for (i=1;i<=N;i++) for (j=1;j<=N;j++) {
39  sup = AddStab(dij[i,j],...);
40  tr2 = OR(tr2,sup);
41  Biddy_KeepFormulaProlonged(tr2,1); /* tr2 is preserved for next cleaning, only */
42  Biddy_Clean(); /* tr2 remains usable */
43 }
44 result = OR(tr1,tr2);
45 Biddy_KeepFormulaUntilPurge(result); /* final result is permanently preserved */
46 Biddy_Clean(); /* tmp results are not needed, anymore */

3.3 MORE DETAILS ON MEMORY MANAGEMENT (SYSTEM AGE AND NODE CHAINING)

Garbage collection is automatically triggered if nodes from all reserved blocks of nodes are used. Garbage collection will remove as many obsolete nodes as possible.

Biddy does not use reference counter but a different approach. We call the implemented algorithm "GC with a system age". It is a variant of a mark-and-sweep approach.

Using system age instead of reference counter has some advantages. It allows GC to be started in any time without breaking the ongoing calculation. Thus, there is no need to taking care of repeating broken calculations. Moreover, the usage of system age instead of reference counter removes all the hassle of referencing and dereferencing nodes and thus it is favorable in an academic package oriented towards simple and readable source code.

There are four classes of nodes. Every node belongs to one of these classes:

  • fortified node (expiry value == 0);
  • fresh node (expiry value == biddySystemAge);
  • prolonged node (expiry value > biddySystemAge);
  • obsolete node (0 < expiry value < biddySystemAge).

Before each GC, nodes must be refreshed in such a way that no successor of a non-obsolete node is obsolete. This is achieved with a relatively simple loop which check every nodes at most once.

Biddy relies on a single hash table for all variables. However, it supports chaining of nodes to form different lists (using an extra pointer in each node). This facility is used to improve efficiency of garbage collection and sifting.

Please node, that node chaining is not determined or limited by using formulae protecting schema or a system age approach, it is an independent mechanism.

### 4. BUILDING PACKAGES

Compiling Biddy library

On GNU/Linux, we are using gcc.

1 biddy> make dynamic
2 biddy> make clean

Alternatively, you can use:

1 biddy> make static
2 biddy> make debug
3 biddy> make profile

You can use specify the target folder:

1 biddy> make dynamic "BINDIR = ./bin"
2 biddy> make clean "BINDIR = ./bin"

On MS Windows, we are using MSYS2. We use pacman to prepare the environment:

1 MSYS shell> pacman -Syuu
2 MSYS shell> pacman -S mingw-w64-i686-gcc
3 MSYS shell> pacman -S mingw-w64-x86_64-gcc
4 MSYS shell> pacman -S make
5 MSYS shell> pacman -S bison
6 MSYS shell> pacman -S gdb
7 MSYS shell> pacman -S nano
8 MSYS shell> pacman -S tar
9 MSYS shell> pacman -S subversion

Alternatively, you can use Visual Studio for building. There is a prepared solution consisting of many projects. You need to adapt include and lib folders.

1 ./VS/Biddy.sln

To produce nice setup files, we use Advanced Installer (http://www.advancedinstaller.com/). We have been granted a free licence. MANY THANKS!

Dependencies

On GNU/Linux, we are using libgmp (https://gmplib.org/).

On MS Windows, we are using MPIR library (http://mpir.org/).

Creating Biddy library as a zip package

1 biddy> ./package-bin

You need a zip program.

On MS Windows, you need 7-Zip (http://7-zip.org/) - and it has a strange use of -x! You also need file 7zsd_All_x64.sfx that you should download as part of "7z SFX Tools" from http://7zsfx.info/en/ and put in the directory containing 7z.exe.

You install the resulting package by extracting libraries to the appropriate directory (may be local, e.g. user's home directory).

When using this package on GNU/Linux, you have to tell bash about the library:

1 export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/absolute/path/to/biddy/library

Creating zip file with source code of a complete Biddy project

1 biddy> ./package-source

If available, source code of bddview and BDD Scout will be included, too.

Creating packages for GNU/Linux

1 biddy> ./package-tgz
2 biddy> ./package-deb
3 biddy> ./package-rpm

These scripts are intedend to be used on Ubuntu. These scripts needs release number as an argument. Script package-tgz must be invoked before running package-deb. Debian packages must be created before RPM packages.

./package-tgz should create orig.tar.gz file and prepare directories for creating debian and RPM packages. You can run ./package-tgz only if version changes.

./package-deb should create debian packages (libbidy and libbiddy-dev). They are tested on Ubuntu system.

./package-rpm should create RPM packages (libbidy and libbiddy-devel). They are tested on openSUSE system.

Creating demo aplication bddscout

You need complete sources for biddy, bddview, and bddscout, Scripts are located in biddy/bddscout.

1 bddscout> ./package-bin
2 bddscout> ./package-tgz
3 bddscout> ./package-deb
4 bddscout> ./package-rpm

package-bin should create BDD Scout (staticaly linked with Biddy library). The script will produce a zip file. You install BDD Scout by simply unzip to the target directory.

./package-tgz should create orig.tar.gz file and prepare directories for creating debian and RPM packages. You can run ./package-tgz only if version changes.

./package-deb should create debian packages (bddscout, bddscout-bra, bddscout-ifip, bddscout-bddtrace, bddscout-ifip-data, and bddscout-bddtrace-data). They are tested on Ubuntu system.

./package-rpm should create RPM packages (bddscout, bddscout-bra, bddscout-ifip, bddscout-bddtrace, bddscout-ifip-data, and bddscout-bddtrace-data). They are tested on openSUSE system.

### 5. HISTORY

Biddy is based on a BDD package written in Pascal in 1992 as a student project. At that time, it was a great work and the paper about it won a second place at IEEE Region Student Paper Contest (Paris-Evry, 1993). The paper was published by IEEE as "A. Casar, R. Meolic. Representation of Boolean functions with ROBDDs. IEEE Student paper contest : regional contest winners 1990-1997 : prize-winning papers demonstrating student excellence worldwide, Piscataway, 2000" and can be obtained from http://research.meolic.com/papers/robdd.pdf

In 1995, this BDD package was rewritten in C. Later, this BDD package become an integral part of EST package, a prototype tool for formal verification of concurrent systems. The homepage for EST project is http://est.meolic.com/

In 2003, BDD package from EST was included in the report presented at 16th Symposium on Integrated Circuits and Systems Design (SBCCI'03). The report is available as a paper "G. Janssen. A Consumer Report on BDD Packages. IBM T.J. Watson Research Center. 2003". Get it from http://doi.ieeecomputersociety.org/10.1109/SBCCI.2003.1232832

In 2006, BDD package in EST got the name Biddy.

In 2007, a main part of Biddy package was extracted from EST forming a separate package called Biddy. The code has been reorganized in such a way, that EST is not using internal structures (e.g. node table) directly but using the provided API only.

In 2007, we created local svn repository for maintaining the source code (not live, anymore).

On May 15, 2008, Biddy v1.0 was released containing also bddview v0.95 (Tcl/Tk BDD viewer) and Bdd Scout v0.90 (demo application).

In 2009, 2010, and 2012 updated versions of Biddy v1.0 were released which added support for debian packaging, support for RPM packaging, fix errors, and improve documentation, packaging, and Tcl/Tk GUI.

In 2012, a research paper about Biddy library appears in Journal of Software (doi:10.4304/jsw.7.6.1358-1366) http://ojs.academypublisher.com/index.php/jsw/article/view/jsw070613581366/

In 2013, Biddy v1.1 was released. Biddy_Edge became a pointer instead of structure and all other structures were optimized.

In 2014, Biddy v1.2 was released. Variable swapping and sifting algorithm were the most significant additions.

In 2014, svn repositories for biddy, bddview and bddscout are moved to Savannah. http://svn.savannah.nongnu.org/viewvc/?root=biddy

In 2015, Biddy v1.3, v.1.4 and v1.5 was released. Various input/output methods have been added. Support for 64-bit arhitectures and support for Visual Studio projects were improved. Biddy got a manager. Many CUDD-like functions have been added. Comment's style changed to support doxygen. HTML and PDF documentation were produced.

Also in 2015, Personal Package Archive ppa:meolic/biddy has been created https://launchpad.net/~meolic/+archive/ubuntu/biddy

Also in 2015, sources became available on GitHub https://github.com/meolic/biddy

In 2016, Biddy v1.6 was released. Formulae are not recursively refreshed all the time, anymore. The size of Node table became resizable.

In 2017, Biddy v1.7 was released (there were 4 minor releases, the last one was Biddy v1.7.4). Terminology has changed a lot, e.g. "formulae counter" became "system age". Added support for ROBDDs without complemented edges, 0-sup-BDDs and Tagged 0-sup-BDDs. Implemented creation and manipulaton of non-anonymous managers. Added manipulation of combination sets. Improved many functionalities, e.g sifting. Many new CUDD-like functions have been added. Moreover, bddview and BDD Scout have been significantly improved.

### 6. PUBLICATIONS

If you find our work useful, please, cite us.