github.com/dalzilio/rudd
Package rudd defines a concrete type for Binary Decision Diagrams (BDD), a data structure used to efficiently represent Boolean functions over a fixed set of variables or, equivalently, sets of Boolean vectors with a fixed size. Each BDD has a fixed number of variables, Varnum, declared when it is initialized (using the method New) and each variable is represented by an (integer) index in the interval [0..Varnum), called a level. Our library support the creation of multiple BDD with possibly different number of variables. Most operations over BDD return a Node; that is a pointer to a "vertex" in the BDD that includes a variable level, and the address of the low and high branch for this node. We use integer to represent the address of Nodes, with the convention that 1 (respectively 0) is the address of the constant function True (respectively False). For the most part, data structures and algorithms implemented in this library are a direct adaptation of those found in the C-library BuDDy, developed by Jorn Lind-Nielsen; we even implemented the same examples than in the BuDDy distribution for benchmarks and regression testing. We provide two possible implementations for BDD that can be selected using build tags. Our default implementation (without build tag) use a standard Go runtime hashmap to encode a "unicity table". When building your executable with the build tag `buddy`, the API will switch to an implementation that is very close to the one of the BuDDy library; based on a specialized data-structure that mix a dynamic array with a hash table. To get access to better statistics about caches and garbage collection, as well as to unlock logging of some operations, you can also compile your executable with the build tag `debug`. The library is written in pure Go, without the need for CGo or any other dependencies. Like with MuDDy, a ML interface to BuDDy, we piggyback on the garbage collection mechanism offered by our host language (in our case Go). We take care of BDD resizing and memory management directly in the library, but "external" references to BDD nodes made by user code are automatically managed by the Go runtime. Unlike MuDDy, we do not provide an interface, but a genuine reimplementation of BDD in Go. As a consequence, we do not suffer from FFI overheads when calling from Go into C. The following is an example of a callback handler, used in a call to Allnodes, that counts the number of active nodes in the whole BDD. The following is an example of a callback handler, used in a call to Allsat, that counts the number of possible assignments (such that we do not count don't care twice). This example shows the basic usage of the package: create a BDD, compute some expressions and output the result.
Readme
RuDD is a library for Binary Decision Diagrams written in pure Go.
RuDD is a Binary Decision Diagram (BDD) library written in pure Go, without the need for CGo or any other dependencies. A BDD is a data structure used to efficiently represent Boolean functions or, equivalently, sets of Boolean vectors.
It has nothing to do with Behaviour Driven Development testing!
We provide two possible implementations for BDD that can be selected using build tags. The rationale for this unorthodox use of build tags is to avoid the use of interfaces, and therefore dynamic dispatch, as well as to favor some automatic compiler optimizations (such as code inlining).
Our default implementation (without any build tags) use a standard Go runtime hashmap to encode a "unicity table".
When building your executable with the build tag buddy (as in go build -tags buddy mycmd) the API will switch to an implementation that is very close to the
one of the BuDDy library; based on a specialized data-structure that mix a
dynamic array with a hash table.
To get access to better statistics about caches and garbage collection, as well as to unlock logging of some operations, you can also compile your executable with the build tag debug.
For the most part, RuDD is a direct translation in Go of the BuDDy C-library developed by Jorn Lind-Nielsen. You can find a high-level description of the algorithms and data-structures used in this project by looking at "An Introduction To Binary Decision Diagrams", a Research Report also distributed as part of the BuDDy distribution. The adaptation was made easy by the simplicity of its architecture (in a good sense) and the legibility of its code.
In many places, the code of RuDD is an almost line-by-line copy of BuDDy (including reusing part of the same comments for documenting the code), with a few adaptations to follow some of Go best practices; we even implement the same examples than in the BuDDy distribution for benchmarks and regression testing.
BuDDy is a mature software library, that has been used on several projects, with performances on par with more complex libraries, such as CUDD. You can find a comparative study of the performances for several BDD libraries in [DHJ+2015].
Like with MuDDy, a ML interface to BuDDy, we piggyback on the garbage collection mechanism offered by our host language. We take care of BDD resizing and memory management directly in the library, but external references to BDD nodes made by user code are automatically managed by the Go runtime. Unlike MuDDy, we do not provide an interface, but a genuine reimplementation of BuDDy. As a consequence, we do not suffer from FFI overheads when calling from Go into C, which is one of the major pain points of working with Go.
Experiences have shown that there is no significant loss of performance when using BuDDy from a functional language with garbage collection, compared to using C or C++ [L09]. For example, we use MuDDy in the tedd model-checker provided with Tina (together with other libraries for dealing with multi-valued decision diagrams). One of our motivations in this project is to see whether we can replicate this experience in Go. Our first experiments show very promising results, but we are still lacking a serious study of the performances of our library.
go get github.com/dalzilio/rudd
The main goal of RuDD is to test the performances of a lightweight BDD library
directly implemented in Go, with a focus on implementing symbolic model-checking
tools. At the moment, we provide only a subset of the functionalities defined in
BuDDy, which is enough for our goals. In particular, we do not provide any
method for the dynamic reordering of variables. We also lack support for Finite
Domain Blocks (fdd) and Boolean Vectors (bvec).
In the future, we plan to add new features to RuDD and to optimize some of its internals. For instance with better caching strategies or with the use of concurrency features. It means that the API could evolve in future releases but that no functions should disappear or change significantly.
The library is named after a fresh water fish, the common rudd (Scardinius erythrophthalmus), or "gardon rouge" in French, that is stronger and more resistant that the common roach, with which it is often confused. While it is sometimes used as bait, its commercial interest is minor. This is certainly a fitting description for our code ! It is also a valid English word ending with DD, which is enough to justify our choice.
You may have a look at the documentation for BuDDy (and MuDDy) to get a good understanding of how the library can be used.
[An97] Henrik Reif Andersen. An Introduction to Binary Decision Diagrams. Lecture Notes for a course on Advanced Algorithms. Technical University of Denmark. 1997.
[L09] Ken Friis Larsen. A MuDDy Experience -– ML Bindings to a BDD Library." IFIP Working Conference on Domain-Specific Languages. Springer, 2009.
[DHJ+2015] Tom van Dijk et al. A comparative study of BDD packages for probabilistic symbolic model checking. International Symposium on Dependable Software Engineering: Theories, Tools, and Applications. Springer, 2015.
You can find several examples in the *_test.go files.
To get access to better statistics about caches and garbage collection, as well
as to unlock logging of some operations, you can compile your executable with
the build tag debug, for instance with a directive such as go run -tags debug mycmd.
package main
import (
"github.com/dalzilio/rudd"
"math/big"
)
func main() {
// create a new BDD with 6 variables, 10 000 nodes and a cache size of 5 000 (initially),
// with an implementation based on the BuDDY approach
bdd := rudd.New(6, Nodesize(10000), Cachesize(5000))
// n1 == x2 & x3 & x5
n1 := bdd.Makeset([]int{2, 3, 5})
// n2 == x1 | !x3 | x4
n2 := bdd.Or(bdd.Ithvar(1), bdd.NIthvar(3), bdd.Ithvar(4))
// n3 == ∃ x2,x3,x5 . (n2 & x3)
n3 := bdd.AndExist(n1, n2, bdd.Ithvar(3))
// you can export a BDD in Graphviz's DOT format
fmt.Printf("Number of sat. assignments: %s\n", bdd.Satcount(n3))
fmt.Println(bdd.Stats())
bdd.Dot(os.Stdout)
}
The library has no dependencies outside of the standard Go library. It uses Go modules and has been tested with Go 1.16.
This software is distributed under the MIT License. A copy of the license agreement is found in the LICENSE file.
The original C code for BuDDy was released under a very permissive license that is included in the accompanying NOTICE file, together with a list of the original authors. While the current implementation of RuDD adds some original work, I expect every redistribution to include the present NOTICE and acknowledge that some source files and examples have been copied and adapted from the BuDDy Binary Decision Diagrams Library, Package v2.4, Copyright (C) 1996-2002 by Jorn Lind-Nielsen (see http://buddy.sourceforge.net/).
FAQs
Package rudd defines a concrete type for Binary Decision Diagrams (BDD), a data structure used to efficiently represent Boolean functions over a fixed set of variables or, equivalently, sets of Boolean vectors with a fixed size. Each BDD has a fixed number of variables, Varnum, declared when it is initialized (using the method New) and each variable is represented by an (integer) index in the interval [0..Varnum), called a level. Our library support the creation of multiple BDD with possibly different number of variables. Most operations over BDD return a Node; that is a pointer to a "vertex" in the BDD that includes a variable level, and the address of the low and high branch for this node. We use integer to represent the address of Nodes, with the convention that 1 (respectively 0) is the address of the constant function True (respectively False). For the most part, data structures and algorithms implemented in this library are a direct adaptation of those found in the C-library BuDDy, developed by Jorn Lind-Nielsen; we even implemented the same examples than in the BuDDy distribution for benchmarks and regression testing. We provide two possible implementations for BDD that can be selected using build tags. Our default implementation (without build tag) use a standard Go runtime hashmap to encode a "unicity table". When building your executable with the build tag `buddy`, the API will switch to an implementation that is very close to the one of the BuDDy library; based on a specialized data-structure that mix a dynamic array with a hash table. To get access to better statistics about caches and garbage collection, as well as to unlock logging of some operations, you can also compile your executable with the build tag `debug`. The library is written in pure Go, without the need for CGo or any other dependencies. Like with MuDDy, a ML interface to BuDDy, we piggyback on the garbage collection mechanism offered by our host language (in our case Go). We take care of BDD resizing and memory management directly in the library, but "external" references to BDD nodes made by user code are automatically managed by the Go runtime. Unlike MuDDy, we do not provide an interface, but a genuine reimplementation of BDD in Go. As a consequence, we do not suffer from FFI overheads when calling from Go into C. The following is an example of a callback handler, used in a call to Allnodes, that counts the number of active nodes in the whole BDD. The following is an example of a callback handler, used in a call to Allsat, that counts the number of possible assignments (such that we do not count don't care twice). This example shows the basic usage of the package: create a BDD, compute some expressions and output the result.
Did you know?
Socket for GitHub automatically highlights issues in each pull request and monitors the health of all your open source dependencies. Discover the contents of your packages and block harmful activity before you install or update your dependencies.
Security News
The June TC39 meeting wrapped up this week with eight proposals moving on to the next stage. Here's a quick roundup of the features that the committee approved to advance.
Security News
Cyber extortion in the US and Canada hit record levels in 2023, with ransomware attacks surging and median ransom demands skyrocketing, though fewer companies are choosing to pay ransoms.
Security News
Ecma TC39 is meeting this week and has moved key ECMAScript proposals forward, advancing Deferred Import Evaluation, Error.isError(), RegExp Escaping, and Promise.try to the next stages.