gobdd

package module
v0.1.0 Latest Latest
Warning

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

 Go to latest Published: Jun 15, 2026 License: MIT Imports: 7 Imported by: 0

README

GOBDD — Zero-Allocation Binary Decision Diagrams for Go

Go Version License Go Report Card GoDoc Coverage Tests

A pure Go implementation of Ordered Binary Decision Diagrams (OBDDs) with zero heap allocations. Every backing array, node table, cache bucket, and temporary slice is allocated through a custom off-heap memory allocator — the Go GC never scans BDD data.

BDDs are a canonical representation of Boolean functions. Two functions are equivalent if and only if their BDDs are structurally identical, enabling O(1) equivalence checking after construction. They underpin symbolic model checking, formal verification, SAT solving, and the modal logic engine in github.com/xDarkicex/logic.

Table of Contents

Why GOBDD

There are no pure-Go BDD libraries with zero heap allocation. Existing options either wrap C libraries through CGo (Buddy, CUDD) or use standard Go allocation patterns that place BDD data structures on the garbage-collected heap. For applications that construct millions of BDD nodes — model checking, bisimulation, symbolic reachability — GC pressure becomes a dominant cost, often exceeding 40% of total runtime.

GOBDD targets that gap:

Property GOBDD CGo wrappers Hypothetical heap-BDD
Pure Go ✅ ❌ ✅
Zero GC pressure ✅ ✅ ❌
Race-clean ✅ varies varies
Buddy API parity ✅ ✅ ✅
ARM64 aligned ✅ n/a ✅
No CGo build flags ✅ ❌ ✅

Zero Heap Allocation

Every allocation in GOBDD uses github.com/xDarkicex/memory — a custom off-heap allocator providing 16-byte aligned memory with Pool, Arena, and ShardedFreeList backends.

Why 16-byte alignment?

ARM64 (Apple Silicon, AWS Graviton) requires 128-bit atomic operations to be 16-byte aligned. Unaligned atomics trap with SIGBUS. The memory allocator guarantees every allocation meets this constraint, making GOBDD safe on ARM64 without GOARM=7 workarounds or alignment padding hacks.

Allocation strategy
Allocator Use in GOBDD
memory.Pool Node table, unique table buckets, op-cache entries, variable ordering arrays, reference counts, temporary visited-tracking slices, serialization remap tables
memory.Arena (reserved for modal integration — frame state, timeline entries)
memory.ShardedFreeList (reserved for modal integration — high-churn tableau nodes)

No make(), no new(), no &T{} for any slice-backed or high-frequency struct. The Go GC traces only the BDD manager struct itself — ~200 bytes total.

Installation

go get github.com/xDarkicex/gobdd@latest

Requires Go 1.25+ and a dependency on github.com/xDarkicex/memory.

Quick Start

package main

import (
    "fmt"

    "github.com/xDarkicex/gobdd"
    "github.com/xDarkicex/memory"
)

func main() {
    pool, _ := memory.NewPool(memory.DefaultConfig())
    defer pool.Reset()

    b := gobdd.New(4, pool) // 4 variables: x0, x1, x2, x3

    x0 := b.Var(0)
    x1 := b.Var(1)
    f := b.And(x0, b.Not(x1)) // x0 ∧ ¬x1

    // Count satisfying assignments
    fmt.Println(b.SatisfyCount(f)) // 4 (x0=1, x1=0, x2=*, x3=*)

    // Find one assignment
    fmt.Println(b.SatisfyOne(f)) // [true false false false]

    // Quantify
    v0only := b.ForAll(f, 0) // ∀x0.(x0∧¬x1) = false
    fmt.Println(v0only == gobdd.False)
}

API Overview

Constructors & Operators
Function Description
New(n, pool) Create BDD manager with n variables
Var(v) BDD for variable v
Nithvar(v) BDD for ¬v
Not(f), And(f,g), Or(f,g) Boolean operators
Xor(f,g), Implies(f,g), Equiv(f,g) Boolean operators
Nand(f,g), Nor(f,g) Boolean operators
ITE(f,g,h) If-then-else: f ? g : h
Apply(f,g,op) Generic binary apply with operator code
Restrict(f,v,val) Cofactor: f[v := val]
RestrictBDD(f,c) BDD-encoded restriction with polarity
Constrain(f,c) Generalized cofactor
Simplify(f,d) Simplify under don't-care set d
Compose(f,v,g) Substitute: f[v := g]
Replace(f,pair) Multi-variable substitution
VecCompose(f,pair) Compose all variables in pair
Quantification
Function Description
Exists(f,v) / ForAll(f,v) Single-variable quantification
ExistsAll(f,vars) / ForAllVars(f,vars) Multi-variable (slice)
ExistSet(f,set) / ForAllSet(f,set) BDD variable set quantification
Unique(f,set) Unique existential: ∃!vars. f
AppEx(f,g,op,vars) / AppAll(...) Apply + quantify
AppExBDD(f,g,op,set) / AppAllBDD(...) BDD varset variants
AppUni(l,r,varset,op) Apply + unique quantify (fused)
Satisfiability & Model Extraction
Function Description
SatisfyOne(f) One satisfying assignment ([]bool)
FullSatOne(f) Assignment for all variables ([]bool)
FullSatOneBDD(f) Full minterm as BDD
SatOne(f) One minterm BDD
SatOneSet(f,set,pol) Minterm respecting variable set
AllSat(f,handler) Enumerate all satisfying assignments
SatisfyCount(f) Count satisfying assignments (uint64)
SatCountDouble(f) Count as float64 (overflow-safe)
SatCountLn(f) Natural log of count
SatCountSet(f,vars) / SatCountLnSet(...) Count over variable set
Information & Debugging
Function Description
Support(f) Variable support ([]int32)
SupportBDD(f) Variable support as BDD set
NodeCount() Total allocated nodes
AnodeCount(roots) Distinct nodes across BDD array
PathCount(f) Number of paths to True terminal
VarProfile(f) Node count per variable level
VarOf(f), Low(f), High(f) Node field accessors
Stats() Comprehensive statistics
PrintDot(f) / FprintDot(w,f) Graphviz DOT output
PrintTable(f) Truth table string
ToDNF(f) / ToCNF(f) / ToFormula(f) Formula string conversion
Variable Sets & Pairs
Function Description
MakeSet(vars) Build BDD variable set from slice
ScanSet(f) Extract variables from BDD set
NewPair() Create substitution pair
Pair.Set(old, new) Map variable → BDD
Pair.SetVar(old, new) Map variable → variable
Pair.SetVars(olds, news, n) Batch variable → variable
Pair.SetAll(olds, news, n) Batch variable → BDD
Pair.Reset() Reset to identity mapping
Reordering
Function Description
SwapVar(v1,v2) Swap two adjacent variables
Sift() Rudell's sifting (full reorder pass)
Serialization
Function Description
Save(w,f) Write buddy-compatible format to io.Writer
Load(r) Read and rebuild from io.Reader
Reference Counting
Function Description
AddRef(f) Increment external reference count
DelRef(f) Decrement external reference count
RefCount(f) Query reference count
Lifecycle & Tuning
Function Description
Done() Release all resources
IsRunning() Check if initialized
SetVarNum(n) / ExtVarNum(n) Resize variable count
SetCacheRatio(r) Resize operator cache

Buddy Parity

GOBDD targets full API parity with Buddy by Jorn Lind-Nielsen.

71 functions implemented covering the complete operational API: all Boolean operators, quantifiers (existential, universal, unique), apply-with-quantify fused operations, restriction, constraint, simplification, composition, substitution, variable sets, pairs, reordering (swap + sift), serialization (save/load), reference counting, and lifecycle management.

The remaining ~10 unimplemented functions are debug-printing variants (bdd_printset, bdd_printall) and advanced reorder methods (WIN2, WIN3, SIFTITE, auto-reorder) not required by downstream consumers.

Architecture

gobdd/
├── bdd.go          BDD manager, unique table, ITE, op-cache
├── types.go        NodeID, OpCode distinct types
├── ops.go          Constrain, Simplify, Apply, BuildCube, PathCount
├── quant.go        ExistSet, ForAllSet, Unique, quantRec, RestrictBDD
├── sat.go          SatOne, FullSatOne, SatOneSet, AllSat
├── replace.go      Pair, Replace, VecCompose, SwapVar
├── reorder.go      Sift (Rudell), swapLevels, Stats
├── serialize.go    Save/Load (buddy-compatible format)
├── refcount.go     AddRef, DelRef, automatic remap during reorder
├── mgmt.go         Done, SetVarNum, ExtVarNum, SetCacheRatio
├── io.go           PrintDot, PrintTable, MakeSet, ScanSet, VarProfile
├── convert.go      ToDNF, ToCNF, ToFormula
└── LICENSES/
    └── buddy.txt   Original Buddy license

Key design decisions:

  • Level indirection (var2level / level2var): Enables atomic variable swap without rebuilding the entire BDD from formula. The node table stores levels (positions), not variables — levels are swapped by updating two arrays.
  • Distinct types (NodeID, OpCode): Go defined types prevent argument transposition (passing an operator code where a node handle is expected). The compiler catches these at build time.
  • Pool-backed unique table: Open-addressing hash table keyed by (level, lo, hi) with multiplicative hashing and power-of-two sizing.
  • ITE memoization: Operator cache avoids recomputing identical ITE subproblems, giving polynomial-time complexity on DAG-structured inputs.
  • Post-order save/load: Serialization format matches Buddy's layout exactly, enabling cross-compatibility.

Testing & Coverage

go test -v -race -cover ./...
  • 95 tests, all passing with -race
  • Covers every exported function with dedicated test cases
  • CI workflow (.github/workflows/test.yml) runs tests, race detector, and publishes a coverage badge to the coverage branch

License & Attribution

GOBDD is a Go port of Buddy by Jorn Lind-Nielsen (1996–2002). The original Buddy library is provided under a permissive MIT-style license that allows modification, redistribution, and re-licensing of derivative works.

This project would not exist without Jorn Lind-Nielsen's elegant BDD implementation, which has served as the reference design for symbolic model checking libraries worldwide for over two decades. Thank you, Jorn.

Documentation

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

This section is empty.

Types

type BDD 

type BDD struct {
	// contains filtered or unexported fields
}

BDD is a manager for Binary Decision Diagrams.

func New 

func New(numVars int, pool *memory.Pool) *BDD

New creates a BDD manager with the given number of variables.

func (*BDD) AddRef 

func (b *BDD) AddRef(f NodeID) NodeID

AddRef increments the external reference count on f. Nodes with positive reference counts are automatically remapped during SwapVar/Sift. Matches buddy bdd_addref (kernel.c:1115).

func (*BDD) AllSat 

func (b *BDD) AllSat(f NodeID, handler func(assign []bool))

func (*BDD) And 

func (b *BDD) And(f, g NodeID) NodeID

func (*BDD) AnodeCount 

func (b *BDD) AnodeCount(roots []NodeID) int

AnodeCount counts distinct nodes across an array of BDDs. Shared nodes are counted only once. Matches buddy bdd_anodecount (bddop.c:2653). CC=4.

func (*BDD) AppAll 

func (b *BDD) AppAll(f, g NodeID, op OpCode, vars []int32) NodeID

func (*BDD) AppAllBDD 

func (b *BDD) AppAllBDD(f, g NodeID, op OpCode, varset NodeID) NodeID

func (*BDD) AppEx 

func (b *BDD) AppEx(f, g NodeID, op OpCode, vars []int32) NodeID

func (*BDD) AppExBDD 

func (b *BDD) AppExBDD(f, g NodeID, op OpCode, varset NodeID) NodeID

func (*BDD) AppUni 

func (b *BDD) AppUni(l, r NodeID, varset NodeID, op OpCode) NodeID

func (*BDD) Apply 

func (b *BDD) Apply(f, g NodeID, op OpCode) NodeID

func (*BDD) BuildCube 

func (b *BDD) BuildCube(vars []int32, positive []bool) NodeID

func (*BDD) Compose 

func (b *BDD) Compose(f NodeID, v int32, g NodeID) NodeID

func (*BDD) Constrain 

func (b *BDD) Constrain(f, c NodeID) NodeID

Constrain returns the generalized cofactor of f with respect to c.

func (*BDD) DelRef 

func (b *BDD) DelRef(f NodeID)

DelRef decrements the external reference count on f. Matches buddy bdd_delref (kernel.c:1141).

func (*BDD) Diff 

func (b *BDD) Diff(f, g NodeID) NodeID

func (*BDD) Done 

func (b *BDD) Done()

Done releases all resources held by the BDD. After Done, the BDD must not be used. Matches buddy bdd_done (bdd.h:231).

func (*BDD) Equiv 

func (b *BDD) Equiv(f, g NodeID) NodeID

func (*BDD) ExistSet 

func (b *BDD) ExistSet(f, varset NodeID) NodeID

func (*BDD) Exists 

func (b *BDD) Exists(f NodeID, v int32) NodeID

func (*BDD) ExistsAll 

func (b *BDD) ExistsAll(f NodeID, vars []int32) NodeID

func (*BDD) ExtVarNum 

func (b *BDD) ExtVarNum(n int32) int32

ExtVarNum adds n new variables and returns the index of the first new variable. Matches buddy bdd_extvarnum (bdd.h:233). CC=2.

func (*BDD) ForAll 

func (b *BDD) ForAll(f NodeID, v int32) NodeID

func (*BDD) ForAllSet 

func (b *BDD) ForAllSet(f, varset NodeID) NodeID

func (*BDD) ForAllVars 

func (b *BDD) ForAllVars(f NodeID, vars []int32) NodeID

func (*BDD) FprintDot 

func (b *BDD) FprintDot(file *os.File, f NodeID)

func (*BDD) FullSatOne 

func (b *BDD) FullSatOne(f NodeID) []bool

func (*BDD) FullSatOneBDD 

func (b *BDD) FullSatOneBDD(f NodeID) NodeID

FullSatOneBDD returns a minterm BDD that implies f, with a variable at every level. Matches buddy bdd_fullsatone (bddop.c:2285). CC=4.

func (*BDD) High 

func (b *BDD) High(f NodeID) NodeID

func (*BDD) IBuildCube 

func (b *BDD) IBuildCube(value int, width int, vars []int32) NodeID

IBuildCube builds a cube from an integer bitmask. The width low-order bits of value encode the polarity of vars[0..width-1]: bit=1 → positive literal, bit=0 → negated literal. The MSB corresponds to vars[0], LSB to vars[width-1]. Matches buddy bdd_ibuildcube (bddop.c:357). CC=3.

func (*BDD) ITE 

func (b *BDD) ITE(f, g, h NodeID) NodeID

func (*BDD) Implies 

func (b *BDD) Implies(f, g NodeID) NodeID

func (*BDD) InvImp 

func (b *BDD) InvImp(f, g NodeID) NodeID

func (*BDD) IsRunning 

func (b *BDD) IsRunning() bool

IsRunning reports whether the BDD is initialized and ready for use. Matches buddy bdd_isrunning (bdd.h:234).

func (*BDD) Less 

func (b *BDD) Less(f, g NodeID) NodeID

func (*BDD) Load 

func (b *BDD) Load(r io.Reader) (NodeID, error)

Load reads a BDD from r in buddy-compatible format. Returns the root NodeID. The BDD's variable ordering is updated. CC=8.

func (*BDD) Low 

func (b *BDD) Low(f NodeID) NodeID

func (*BDD) MakeSet 

func (b *BDD) MakeSet(vars []int32) NodeID

func (*BDD) Nand 

func (b *BDD) Nand(f, g NodeID) NodeID

func (*BDD) NewPair 

func (b *BDD) NewPair() *Pair

func (*BDD) Nithvar 

func (b *BDD) Nithvar(v int32) NodeID

func (*BDD) NodeCount 

func (b *BDD) NodeCount() int

NodeCount returns the total number of allocated nodes.

func (*BDD) Nor 

func (b *BDD) Nor(f, g NodeID) NodeID

func (*BDD) Not 

func (b *BDD) Not(f NodeID) NodeID

func (*BDD) Or 

func (b *BDD) Or(f, g NodeID) NodeID

func (*BDD) PathCount 

func (b *BDD) PathCount(f NodeID) float64

func (*BDD) PrintDot 

func (b *BDD) PrintDot(f NodeID)

func (*BDD) PrintTable 

func (b *BDD) PrintTable(f NodeID) string

func (*BDD) RefCount 

func (b *BDD) RefCount(f NodeID) int32

RefCount returns the external reference count for f.

func (*BDD) RelProd 

func (b *BDD) RelProd(f, g NodeID, vars []int32) NodeID

func (*BDD) RelProdBDD 

func (b *BDD) RelProdBDD(f, g NodeID, varset NodeID) NodeID

func (*BDD) Replace 

func (b *BDD) Replace(f NodeID, p *Pair) NodeID

func (*BDD) Restrict 

func (b *BDD) Restrict(f NodeID, v int32, value bool) NodeID

func (*BDD) RestrictBDD 

func (b *BDD) RestrictBDD(f, c NodeID) NodeID

func (*BDD) SatCountDouble 

func (b *BDD) SatCountDouble(f NodeID) float64

SatCountDouble returns the number of satisfying assignments as float64. Matches buddy bdd_satcount (bddop.c:2460).

func (*BDD) SatCountLn 

func (b *BDD) SatCountLn(f NodeID) float64

func (*BDD) SatCountLnSet 

func (b *BDD) SatCountLnSet(f NodeID, vars []int32) float64

func (*BDD) SatCountSet 

func (b *BDD) SatCountSet(f NodeID, vars []int32) uint64

func (*BDD) SatOne 

func (b *BDD) SatOne(f NodeID) NodeID

func (*BDD) SatOneSet 

func (b *BDD) SatOneSet(f, varset NodeID, pol bool) NodeID

func (*BDD) SatisfyCount 

func (b *BDD) SatisfyCount(f NodeID) uint64

func (*BDD) SatisfyOne 

func (b *BDD) SatisfyOne(f NodeID) []bool

func (*BDD) Save 

func (b *BDD) Save(w io.Writer, f NodeID) error

Save writes a BDD to w in buddy-compatible format. Terminals are written as "0 0 <value>\n". Non-terminals write the node count, variable ordering, then each node in DFS post-order (children before parent). CC=5.

func (*BDD) ScanSet 

func (b *BDD) ScanSet(f NodeID) []int32

func (*BDD) SetCacheRatio 

func (b *BDD) SetCacheRatio(ratio int)

SetCacheRatio sets the operator cache size relative to the node table. The cache is resized to len(nodes) * ratio, clamped to [1024, 262144]. Matches buddy bdd_setcacheratio (bddop.c:276). CC=4.

func (*BDD) SetVarNum 

func (b *BDD) SetVarNum(num int32)

SetVarNum changes the number of variables. If num > current, new variables are added with identity level mapping. If num < current, variables beyond num are removed. Matches buddy bdd_setvarnum (bdd.h:232). CC=7.

func (*BDD) Sift 

func (bd *BDD) Sift()

func (*BDD) Simplify 

func (b *BDD) Simplify(f, d NodeID) NodeID

func (*BDD) Stats 

func (b *BDD) Stats() Stats

func (*BDD) Support 

func (b *BDD) Support(f NodeID) []int32

func (*BDD) SupportBDD 

func (b *BDD) SupportBDD(f NodeID) NodeID

SupportBDD returns the support of f as a BDD variable set. Matches buddy bdd_support (bddop.c:2053).

func (*BDD) SwapVar 

func (b *BDD) SwapVar(v1, v2 int32) func(oldIdx NodeID) NodeID

func (*BDD) ToCNF 

func (b *BDD) ToCNF(f NodeID) string

func (*BDD) ToDNF 

func (b *BDD) ToDNF(f NodeID) string

func (*BDD) ToFormula 

func (b *BDD) ToFormula(f NodeID) string

func (*BDD) Unique 

func (b *BDD) Unique(f, varset NodeID) NodeID

func (*BDD) Var 

func (b *BDD) Var(v int32) NodeID

func (*BDD) VarCount 

func (b *BDD) VarCount() int32

func (*BDD) VarOf 

func (b *BDD) VarOf(f NodeID) int32

func (*BDD) VarProfile 

func (b *BDD) VarProfile(f NodeID) []int32

func (*BDD) VecCompose 

func (b *BDD) VecCompose(f NodeID, p *Pair) NodeID

func (*BDD) Xor 

func (b *BDD) Xor(f, g NodeID) NodeID

type NodeID 

type NodeID int32

NodeID is a handle to a BDD node. Terminal nodes are False (0) and True (1). Non-terminal nodes have indices >= 2. 

const (
	False NodeID = 0
	True  NodeID = 1
)

Terminal node constants.

type OpCode 

type OpCode int32

OpCode is a binary operator code for Apply, AppEx, AppAll, AppUni, and RelProd. 

const (
	OpAnd       OpCode = 0
	OpXor       OpCode = 1
	OpOr        OpCode = 2
	OpNand      OpCode = 3
	OpNor       OpCode = 4
	OpImp       OpCode = 5
	OpBiimp     OpCode = 6
	OpDiff      OpCode = 7
	OpLess      OpCode = 8
	OpInvImp    OpCode = 9
	OpConstrain OpCode = 100
	OpSimplify  OpCode = 101
)

Operator constants for Apply.

type Pair 

type Pair struct {
	// contains filtered or unexported fields
}

func (*Pair) Reset 

func (p *Pair) Reset()

func (*Pair) Set 

func (p *Pair) Set(oldVar int32, newVal NodeID)

func (*Pair) SetAll 

func (p *Pair) SetAll(oldVars []int32, newVals []NodeID, n int)

func (*Pair) SetVar 

func (p *Pair) SetVar(oldVar, newVar int32)

func (*Pair) SetVars 

func (p *Pair) SetVars(oldVars, newVars []int32, n int)

SetVars sets multiple variable-to-variable mappings. oldVars and newVars are variable indices. Matches buddy bdd_setpairs (pairs.c:252).

type Stats 

type Stats struct {
	NodeCount    int
	VarCount     int
	PerVar       [256]int
	EdgesToFalse int
	EdgesToTrue  int
}

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.