gorobdd

README

This is an evolving package for working with Reduced Ordered Binary Decision
Diagrams. Details of the data structure can be found at:
 - http://people.cs.aau.dk/~srba/courses/SV-08/material/09.pdf

Plan of action:
Sequential operations phase:
 - Begin with simple BDD operations. [COMPLETE]
 - Implement BDD --> ROBDD conversion, update operations to use this conversion
   resulting in ROBDDs. [IN PROGRESS]
 - Add helpers to measure operations cost in various terms:
   - Total number of nodes at the end of the operation
   - Maximum number of nodes during the operation
   - Time taken per operation
 - Implement direct ROBDD construction and optimized ROBDD --> ROBDD operations,
 - Add comparison tests, fuzz tests for the two implementations so far.
 - Implement concurrent implementations for these operations, and add comparison
   tests.

Documentation

Overview

Package gorobdd is an implementation of Reduced Ordered Binary Decision Diagrams.

This package is intended to implement ROBDD operations in a few different ways for comparison and fun. Details about the data structure can be found at:

• http://people.cs.aau.dk/~srba/courses/SV-08/material/09.pdf

Index

• func CountNodes(b *ROBDD) (int, error)
• func Equal(a *ROBDD, b *ROBDD) (bool, error)
• func GraphEqual(a *ROBDD, b *ROBDD) (bool, error)
• type ROBDD
  • func And(a *ROBDD, b *ROBDD) (*ROBDD, error)
  • func False(voc []string) *ROBDD
  • func FromTuples(voc []string, tuples [][]bool) (*ROBDD, error)
  • func Not(a *ROBDD) (*ROBDD, error)
  • func Or(a *ROBDD, b *ROBDD) (*ROBDD, error)
  • func Reduce(a *ROBDD) (*ROBDD, error)
  • func True(voc []string) *ROBDD
  • func (b ROBDD) String() string

Functions

func CountNodes

func CountNodes(b *ROBDD) (int, error)

CountNodes counts the total number of unique BDD nodes in the given ROBDD.

func Equal

func Equal(a *ROBDD, b *ROBDD) (bool, error)

Equal determines if two ROBDDs correspond to equivalent boolean expressions.

func GraphEqual

func GraphEqual(a *ROBDD, b *ROBDD) (bool, error)

GraphEqual determines if two ROBDDs are structurally identical. GraphEqual implies Equal.

Types

type ROBDD

type ROBDD struct {
	// Names for all the plys.
	// Order of vocabulary is significant.
	Vocabulary []string
	*node.Node
}

ROBDD is short for Reduced Ordered Binary Decision Diagram, a concise normalized representation of boolean formulas. It is a DAG. Internal nodes have two branches labeled True and False, and unique True and/or False leafs. Additionally, each internal node is labeled with a variable from a given vocabulary, and variables from the vocabulary occur in a fixed order (skipping some) on any path down the DAG. The order in which vocabulary names match the plys can be changed.

func And

func And(a *ROBDD, b *ROBDD) (*ROBDD, error)

And computes the conjuction of the boolean expressions corresponding to given BDDs.

func False

func False(voc []string) *ROBDD

False returns the ROBDD with value False for the given vocabulary.

func FromTuples

func FromTuples(voc []string, tuples [][]bool) (*ROBDD, error)

FromTuples allows constructing a ROBDD from a boolean expression in DNF. voc is the vocabulary to be used for the ROBDD. tuples lists the values assumed by each ply for which the expression evaluates to True.

func Not

func Not(a *ROBDD) (*ROBDD, error)

Not computes the negation of the boolean expression corresponding to given ROBDD.

func Or

func Or(a *ROBDD, b *ROBDD) (*ROBDD, error)

Or computes the disjunction of the boolean expressions corresponding to given BDDs.

func Reduce

func Reduce(a *ROBDD) (*ROBDD, error)

Reduce converts an ROBDD in place to the the reduced canonicalized form. Returns the reduced ROBDD.

func True

func True(voc []string) *ROBDD

True returns the ROBDD with value True for the given vocabulary.

func (ROBDD) String

func (b ROBDD) String() string

String is part of the implementation of Stringer interface.