rudd

package module
v1.1.0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: May 21, 2021 License: MIT Imports: 11 Imported by: 0

README


Logo

RuDD Go Report Card GoDoc Release

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

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

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 

func New(varnum int, options ...func(*configs)) (*BDD, error)

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 

func (b *BDD) Allnodes(f func(id, level, low, high int) error, n ...Node) error

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 

func (b *BDD) Allsat(f func([]int) error, n Node) error

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 

func (b *BDD) And(n ...Node) Node

And returns the logical 'and' of a sequence of nodes or, equivalently, computes the intersection of a sequence of Boolean vectors.

func (*BDD) AndExist 

func (b *BDD) AndExist(varset, n1, n2 Node) Node

AndExist returns the "relational composition" of two nodes with respect to varset, meaning the result of (∃ varset . n1 & n2).

func (*BDD) AppEx 

func (b *BDD) AppEx(n1, n2 Node, op Operator, varset Node) Node

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 

func (b *BDD) Apply(n1, n2 Node, op Operator) Node

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 

func (b *BDD) Dot(w io.Writer, n ...Node) error

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) Equal 

func (b *BDD) Equal(n1, n2 Node) bool

Equal tests equivalence between nodes.

func (*BDD) Equiv 

func (b *BDD) Equiv(n1, n2 Node) Node

Equiv returns the logical 'bi-implication' between two BDDs.

func (*BDD) Error 

func (b *BDD) Error() string

Error returns the error status of the BDD.

func (*BDD) Errored 

func (b *BDD) Errored() bool

Errored returns true if there was an error during a computation.

func (*BDD) Exist 

func (b *BDD) Exist(n, varset Node) Node

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) False 

func (b *BDD) False() Node

False returns the constant false BDD (a node pointing to the value 0).

func (*BDD) From 

func (b *BDD) From(v bool) Node

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 

func (b *BDD) High(n Node) Node

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) Imp 

func (b *BDD) Imp(n1, n2 Node) Node

Imp returns the logical 'implication' between two BDDs.

func (*BDD) Ite 

func (b *BDD) Ite(f, g, h Node) Node

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 

func (b *BDD) Ithvar(i int) Node

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 

func (b *BDD) Label(n Node) int

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 

func (b *BDD) Low(n Node) Node

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 

func (b *BDD) Makeset(varset []int) Node

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 

func (b *BDD) NIthvar(i int) Node

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 

func (b *BDD) NewReplacer(oldvars, newvars []int) (Replacer, error)

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 

func (b *BDD) Not(n Node) Node

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 

func (b *BDD) Or(n ...Node) Node

Or returns the logical 'or' of a sequence of nodes or, equivalently, computes the union of a sequence of Boolean vectors.

func (*BDD) Print 

func (b *BDD) Print(w io.Writer, n ...Node)

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 

func (b *BDD) Replace(n Node, r Replacer) Node

Replace takes a Replacer and computes the result of n after replacing old variables with new ones. See type Replacer.

func (*BDD) Satcount 

func (b *BDD) Satcount(n Node) *big.Int

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 

func (b *BDD) Scanset(n Node) []int

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 

func (b *BDD) Stats() string

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'.

func (*BDD) True 

func (b *BDD) True() Node

True returns the constant true BDD (a node pointing to the value 1). Our implementation ensures that this pointer is unique. Hence two successive call to True should return the same node.

func (*BDD) Varnum 

func (b *BDD) Varnum() int

Varnum returns the number of defined variables.

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. 

const (
	OPand Operator = iota
	OPxor
	OPor
	OPnand
	OPnor
	OPimp
	OPbiimp
	OPdiff
	OPless
	OPinvimp
)

func (Operator) String 

func (op Operator) String() string

type Replacer 

type Replacer interface {
	Replace(int32) (int32, bool)
	Id() int
}

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

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.