README
¶
RuDD 
RuDD is a library for Binary Decision Diagrams written in pure Go.
About
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!
Specific use of Go build tags
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.
Relation with BuDDy and MuDDy
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.
Installation
go get github.com/dalzilio/rudd
Overview
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.
Why this name
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.
References
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.
Usage
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)
}
Dependencies
The library has no dependencies outside of the standard Go library. It uses Go modules and has been tested with Go 1.16.
License
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/).
Authors
- Silvano DAL ZILIO - LAAS/CNRS
Documentation
¶
Overview ¶
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.
Basics ¶
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).
Use of build tags ¶
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`.
Automatic memory management ¶
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.
Example (Allnodes) ¶
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.
package main
import (
"fmt"
"github.com/dalzilio/rudd"
)
func main() {
bdd, _ := rudd.New(5)
n := bdd.AndExist(bdd.Makeset([]int{2, 3}),
bdd.Or(bdd.Ithvar(1), bdd.NIthvar(3), bdd.Ithvar(4)),
bdd.Ithvar(3))
acc := new(int)
count := func(id, level, low, high int) error {
*acc++
return nil
}
bdd.Allnodes(count)
fmt.Printf("Number of active nodes in BDD is %d\n", *acc)
*acc = 0
bdd.Allnodes(count, n)
fmt.Printf("Number of active nodes in node is %d", *acc)
}
Output: Number of active nodes in BDD is 16 Number of active nodes in node is 2
Example (Allsat) ¶
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).
package main
import (
"fmt"
"github.com/dalzilio/rudd"
)
func main() {
bdd, _ := rudd.New(5)
// n == ∃ x2,x3 . (x1 | !x3 | x4) & x3
n := bdd.AndExist(bdd.Makeset([]int{2, 3}),
bdd.Or(bdd.Ithvar(1), bdd.NIthvar(3), bdd.Ithvar(4)),
bdd.Ithvar(3))
acc := new(int)
bdd.Allsat(func(varset []int) error {
*acc++
return nil
}, n)
fmt.Printf("Number of sat. assignments (without don't care) is %d", *acc)
}
Output: Number of sat. assignments (without don't care) is 2
Example (Basic) ¶
This example shows the basic usage of the package: create a BDD, compute some expressions and output the result.
package main
import (
"fmt"
"log"
"github.com/dalzilio/rudd"
)
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, rudd.Nodesize(10000), rudd.Cachesize(3000))
// n1 is a set comprising the three variables {x2, x3, x5}. It can also be
// interpreted as the Boolean expression: 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 print the result or export a BDD in Graphviz's DOT format
log.Print("\n" + bdd.Stats())
fmt.Printf("Number of sat. assignments is %s\n", bdd.Satcount(n3))
}
Output: Number of sat. assignments is 48
Index ¶
- func Cacheratio(ratio int) func(*configs)
- func Cachesize(size int) func(*configs)
- func Maxnodeincrease(size int) func(*configs)
- func Maxnodesize(size int) func(*configs)
- func Minfreenodes(ratio int) func(*configs)
- func Nodesize(size int) func(*configs)
- type BDD
- func (b *BDD) Allnodes(f func(id, level, low, high int) error, n ...Node) error
- func (b *BDD) Allsat(f func([]int) error, n Node) error
- func (b *BDD) And(n ...Node) Node
- func (b *BDD) AndExist(varset, n1, n2 Node) Node
- func (b *BDD) AppEx(n1, n2 Node, op Operator, varset Node) Node
- func (b *BDD) Apply(n1, n2 Node, op Operator) Node
- func (b *BDD) Dot(w io.Writer, n ...Node) error
- func (b *BDD) Equal(n1, n2 Node) bool
- func (b *BDD) Equiv(n1, n2 Node) Node
- func (b *BDD) Error() string
- func (b *BDD) Errored() bool
- func (b *BDD) Exist(n, varset Node) Node
- func (b *BDD) False() Node
- func (b *BDD) From(v bool) Node
- func (b *BDD) High(n Node) Node
- func (b *BDD) Imp(n1, n2 Node) Node
- func (b *BDD) Ite(f, g, h Node) Node
- func (b *BDD) Ithvar(i int) Node
- func (b *BDD) Label(n Node) int
- func (b *BDD) Low(n Node) Node
- func (b *BDD) Makeset(varset []int) Node
- func (b *BDD) NIthvar(i int) Node
- func (b *BDD) NewReplacer(oldvars, newvars []int) (Replacer, error)
- func (b *BDD) Not(n Node) Node
- func (b *BDD) Or(n ...Node) Node
- func (b *BDD) Print(w io.Writer, n ...Node)
- func (b *BDD) Replace(n Node, r Replacer) Node
- func (b *BDD) Satcount(n Node) *big.Int
- func (b *BDD) Scanset(n Node) []int
- func (b *BDD) Stats() string
- func (b *BDD) True() Node
- func (b *BDD) Varnum() int
- type Node
- type Operator
- type Replacer
Examples ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func Cacheratio ¶
func Cacheratio(ratio int) func(*configs)
Cacheratio is a configuration option (function). Used as a parameter in New it sets a "cache ratio" (%) so that caches can grow each time we resize the node table. With a cache ratio of r, we have r available entries in the cache for every 100 slots in the node table. (A typical value for the cache ratio is 25% or 20%). The default value (0) means that the cache size never grows.
func Cachesize ¶
func Cachesize(size int) func(*configs)
Cachesize is a configuration option (function). Used as a parameter in New it sets the initial number of entries in the operation caches. The default value is 10 000. Typical values for nodesize are 10 000 nodes for small test examples and up to 1 000 000 nodes for large examples. See also the Cacheratio config.
func Maxnodeincrease ¶
func Maxnodeincrease(size int) func(*configs)
Maxnodeincrease is a configuration option (function). Used as a parameter in New it sets a limit on the increase in size of the node table. Below this limit we typically double the size of the node list each time we need to resize it. The default value is about a million nodes. Set the value to zero to avoid imposing a limit.
func Maxnodesize ¶
func Maxnodesize(size int) func(*configs)
Maxnodesize is a configuration option (function). Used as a parameter in New it sets a limit to the number of nodes in the BDD. An operation trying to raise the number of nodes above this limit will generate an error and return a nil Node. The default value (0) means that there is no limit. In which case allocation can panic if we exhaust all the available memory.
func Minfreenodes ¶
func Minfreenodes(ratio int) func(*configs)
Minfreenodes is a configuration option (function). Used as a parameter in New it sets the ratio of free nodes (%) that has to be left after a Garbage Collection event. When there is not enough free nodes in the BDD, we try reclaiming unused nodes. With a ratio of, say 25, we resize the table if the number a free nodes is less than 25% of the capacity of the table (see Maxnodesize and Maxnodeincrease). The default value is 20%.
func Nodesize ¶
func Nodesize(size int) func(*configs)
Nodesize is a configuration option (function). Used as a parameter in New it sets a preferred initial size for the node table. The size of the BDD can increase during computation. By default we create a table large enough to include the two constants and the "variables" used in the call to Ithvar and NIthvar.
Types ¶
type BDD ¶
type BDD struct {
// contains filtered or unexported fields
}
BDD is the type of Binary Decision Diagrams. It abstracts and encapsulates the internal states of a BDD; such as caches, or the internal node and unicity tables for example. We propose multiple implementations (two at the moment) all based on approaches where we use integers as the key for Nodes.
func New ¶
New returns a new BDD based on an implementation selected with the build tag; meaning the 'Hudd'-style BDD by default (based on the standard runtime hashmap) or a 'BuDDy'-style BDD if tags buddy is set. Parameter varnum is the number of variables in the BDD.
It is possible to set optional (configuration) parameters, such as the size of the initial node table (Nodesize) or the size for caches (Cachesize), using configs functions. The initial number of nodes is not critical since the table will be resized whenever there are too few nodes left after a garbage collection. But it does have some impact on the efficiency of the operations. We return a nil value if there is an error while creating the BDD.
func (*BDD) Allnodes ¶
Allnodes applies function f over all the nodes accessible from the nodes in the sequence n..., or all the active nodes if n is absent (len(n) == 0). The parameters to function f are the id, level, and id's of the low and high successors of each node. The two constant nodes (True and False) have always the id 1 and 0, respectively. The order in which nodes are visited is not specified. The behavior is very similar to the one of Allsat. In particular, we stop the computation and return an error if f returns an error at some point.
func (*BDD) Allsat ¶
Allsat Iterates through all legal variable assignments for n and calls the function f on each of them. We pass an int slice of length varnum to f where each entry is either 0 if the variable is false, 1 if it is true, and -1 if it is a don't care. We stop and return an error if f returns an error at some point.
func (*BDD) And ¶
And returns the logical 'and' of a sequence of nodes or, equivalently, computes the intersection of a sequence of Boolean vectors.
func (*BDD) AndExist ¶
AndExist returns the "relational composition" of two nodes with respect to varset, meaning the result of (∃ varset . n1 & n2).
func (*BDD) AppEx ¶
AppEx applies the binary operator *op* on the two operands, n1 and n2, then performs an existential quantification over the variables in varset; meaning it computes the value of (∃ varset . n1 op n2). This is done in a bottom up manner such that both the apply and quantification is done on the lower nodes before stepping up to the higher nodes. This makes AppEx much more efficient than an apply operation followed by a quantification. Note that, when *op* is a conjunction, this operation returns the relational product of two BDDs.
func (*BDD) Apply ¶
Apply performs all of the basic bdd operations with two operands, such as AND, OR etc. Operator opr must be one of the following:
Identifier Description Truth table OPand logical and [0,0,0,1] OPxor logical xor [0,1,1,0] OPor logical or [0,1,1,1] OPnand logical not-and [1,1,1,0] OPnor logical not-or [1,0,0,0] OPimp implication [1,1,0,1] OPbiimp equivalence [1,0,0,1] OPdiff set difference [0,0,1,0] OPless less than [0,1,0,0] OPinvimp reverse implication [1,0,1,1]
func (*BDD) Dot ¶
Dot writes a graph-like description of the BDD with roots in n to an output stream using Graphviz's dot format. The behavior of Dot is very similar to the one of Print. In particular, we include all the active nodes of b if n is absent (len(n) == 0).
func (*BDD) Exist ¶
Exist returns the existential quantification of n for the variables in varset, where varset is a node built with a method such as Makeset. We return nil and set the error flag in b if there is an error.
func (*BDD) From ¶
From returns a (constant) Node from a boolean value. We return the (BDD) value True if v is true and False otherwise.
func (*BDD) High ¶
High returns the true (or high) branch of a BDD. We return nil and set the error flag in the BDD if there is an error.
func (*BDD) Ite ¶
Ite (short for if-then-else operator) computes the BDD for the expression [(f & g) | (!f & h)] more efficiently than doing the three operations separately.
func (*BDD) Ithvar ¶
Ithvar returns a BDD representing the i'th variable on success (the expression xi), otherwise we set the error status in the BDD and returns the nil node. The requested variable must be in the range [0..Varnum).
func (*BDD) Label ¶
Label returns the variable (index) corresponding to node n in the BDD. We set the BDD to its error state and return -1 if we try to access a constant node.
func (*BDD) Low ¶
Low returns the false (or low) branch of a BDD. We return nil and set the error flag in the BDD if there is an error.
func (*BDD) Makeset ¶
Makeset returns a node corresponding to the conjunction (the cube) of all the variable in varset, in their positive form. It is such that scanset(Makeset(a)) == a. It returns False and sets the error condition in b if one of the variables is outside the scope of the BDD (see documentation for function *Ithvar*).
func (*BDD) NIthvar ¶
NIthvar returns a node representing the negation of the i'th variable on success (the expression !xi), otherwise the nil node. See *ithvar* for further info.
func (*BDD) NewReplacer ¶
NewReplacer returns a Replacer that can be used for substituting variable oldvars[k] with newvars[k] in the BDD b. We return an error if the two slices do not have the same length or if we find the same index twice in either of them. All values must be in the interval [0..Varnum).
func (*BDD) Not ¶
Not returns the negation of the expression corresponding to node n; it computes the result of !n. We negate a BDD by exchanging all references to the zero-terminal with references to the one-terminal and vice versa.
func (*BDD) Or ¶
Or returns the logical 'or' of a sequence of nodes or, equivalently, computes the union of a sequence of Boolean vectors.
func (*BDD) Print ¶
Print writes a textual representation of the BDD with roots in n to an output stream. The result is a table with rows giving the levels and ids of the nodes and its low and high part.
We print all the nodes in b if n is absent (len(n) == 0), so a call to b.Print(os.Stdout) prints a table containing all the active nodes of the BDD to the standard output. We also simply print the string "True" and "False", respectively, if len(n) == 1 and n[0] is the constant True or False.
func (*BDD) Replace ¶
Replace takes a Replacer and computes the result of n after replacing old variables with new ones. See type Replacer.
func (*BDD) Satcount ¶
Satcount computes the number of satisfying variable assignments for the function denoted by n. We return a result using arbitrary-precision arithmetic to avoid possible overflows. The result is zero (and we set the error flag of b) if there is an error.
func (*BDD) Scanset ¶
Scanset returns the set of variables (levels) found when following the high branch of node n. This is the dual of function Makeset. The result may be nil if there is an error and it is sorted following the natural order between levels.
func (*BDD) Stats ¶
Stats returns information about the BDD. It is possible to print more information about the caches and memory footprint of the BDD by compiling your executable with the build tag 'debug'.
type Node ¶
type Node *int
Node is a reference to an element of a BDD. It represents the atomic unit of interactions and computations within a BDD.
type Operator ¶
type Operator int
Operator describe the potential (binary) operations available on an Apply. Only the first four operators (from OPand to OPnand) can be used in AppEx.
type Replacer ¶
Replacer is the types of substitution objects used in a Replace operation, that substitutes variables in a BDD "function". The only method returning an object of this type is the NewReplacer method. The result obtained when using a replacer created from a BDD, in a Replace operation over a different BDD is unspecified.
Source Files