The trivialib.bdd Reference Manual

Table of Contents

Next: , Previous: , Up: (dir)   [Contents][Index]

The trivialib.bdd Reference Manual

This is the trivialib.bdd Reference Manual, version 0.1, generated automatically by Declt version 2.4 "Will Decker" on Wed Jun 20 12:42:51 2018 GMT+0.


Next: , Previous: , Up: Top   [Contents][Index]

1 Introduction


* Trivialib.Bdd 

Functional implementation of (Ordered) Binary Decision Diagram (BDD) and Zero-suppressed Binary Decision Diagram (ZDD).

+ Bryant, Randal E. "Graph-based algorithms for boolean function
  manipulation." Computers, IEEE Transactions on 100.8 (1986): 677-691.
+ Minato, Shin-ichi. "Zero-suppressed BDDs for set manipulation in
  combinatorial problems." Design Automation, 1993. 30th Conference
  on. IEEE, 1993.

[[http://users.cecs.anu.edu.au/~ssanner/AAAI16/][Tutorial slide]] on Symbolic Methods for Hybrid Inference, Optimization, and Decision-making at AAAI 2016, by [[http://users.cecs.anu.edu.au/~ssanner/][Scott Sanner]]

* FEATURES

Based on structures --- moderately fast

Weak hash table --- GC-aware, moderate memory usage

Pattern matching --- functional, clean implementation

* TODOs

+ more useful interfaces for set manipulation, function manipulation
+ speed
+ extension to ADD (Algebraic Decision Diagram) --- mostly trivial
+ extension to XADD (algebraic decision diagram)
+ extension to MV-DDs (multi-valued decision diagram)
+ extension to AADDs (affine algebrainc decision diagram) --- for representing formula
+ extension to XADDs (continuous variable extension of algebrainc decision diagram) --- for continuous range
+ extension to SDD (sentensial decision diagram)

* Usage

Web API Documentation will be available at http://quickdocs.org/trivialib.bdd/

#+BEGIN_SRC lisp

;; Knuth Chapter 4, figure 12 (and 122), rightmost ("kernel")
;; represent a set {{1,3,5},{1,4},{2,4,6},{2,5},{3,6}}
(labels ((add2 (dd1 dd2) (odd-apply dd1 dd2 (lambda (a b) (or a b))))
         (mul2 (dd1 dd2) (odd-apply dd1 dd2 (lambda (a b) (and a b))))
         (add (dd1 dd2 &rest args)
           (if args
               (apply #'add (add2 dd1 dd2) args)
               (add2 dd1 dd2)))
         (mul (dd1 dd2 &rest args)
           (if args
               (apply #'mul (mul2 dd1 dd2) args)
               (mul2 dd1 dd2)))
         (o (x) (odd (unit x)))
         (x (x) (odd (!unit x)))
         (change-many (node &rest args) (reduce #'change args :initial-value node)))

  (with-odd-context (:variable '(a b c d e f))
    ;; stored into VARIABLES slot of an ODD. ^^^
    ;; Different variable orderings make ODDs incompatible.
    (gcprint
     ;; using BDD reduction rule: 15 nodes
     (add (mul (o 1) (x 2) (o 3) (x 4) (o 5) (x 6))
          (mul (o 1) (x 2) (x 3) (o 4) (x 5) (x 6))
          (mul (x 1) (o 2) (x 3) (o 4) (x 5) (o 6))
          (mul (x 1) (o 2) (x 3) (x 4) (o 5) (x 6))
          (mul (x 1) (x 2) (o 3) (x 4) (x 5) (o 6)))))
  (with-odd-context (:operation #'zdd-apply)
    ;; Different reduction rule also make ODDs incompatible.
    (gcprint
     ;; using Zero-suppressed reduction rule: 8 nodes
     (add (odd (change-many (leaf t) 1 3 5))
          (odd (change-many (leaf t) 1 4))
          (odd (change-many (leaf t) 2 4 6))
          (odd (change-many (leaf t) 2 5))
          (odd (change-many (leaf t) 3 6)))))
  (with-odd-context (:operation #'zdd-apply)
    ;; using a utility function for ZDD
    (gcprint
     (add (odd (make-set '(1 3 5)))
          (odd (make-set '(1 4)))
          (odd (make-set '(2 4 6)))
          (odd (make-set '(2 5)))
          (odd (make-set '(3 6))))))
  (with-odd-context (:operation #'zdd-apply)
    ;; using a utility function for ZDD
    (gcprint
     (odd (make-family '((1 3 5)
                         (1 4)
                         (2 4 6)
                         (2 5)
                         (3 6)))))))
#+END_SRC

** Dependencies

This library is at least tested on implementation listed below:

+ SBCL 1.2.8 on X86-64 Linux  3.13.0-46-generic (author's environment)

Also, it depends on the following libraries:

+ alexandria by  ::
    Alexandria is a collection of portable public domain utilities.

+ trivia by Masataro Asai ::
    NON-optimized pattern matcher compatible with OPTIMA, with extensible optimizer interface and clean codebase

+ immutabe-struct by Masataro Asai :: 

+ trivial-garbage :: For handling weak hash tables.
    
** Author

+ Masataro Asai (guicho2.71828@gmail.com)

* Copyright

Copyright (c) 2015 Masataro Asai (guicho2.71828@gmail.com)


* License

Licensed under the LLGPL License.





Next: , Previous: , Up: Top   [Contents][Index]

2 Systems

The main system appears first, followed by any subsystem dependency.


Previous: , Up: Systems   [Contents][Index]

2.1 trivialib.bdd

Author

Masataro Asai

Contact

guicho2.71828@gmail.com

License

LLGPL

Description

BDD and ZDD implementation using Trivia

Version

0.1

Dependencies
Source

trivialib.bdd.asd (file)

Components

Next: , Previous: , Up: Top   [Contents][Index]

3 Files

Files are sorted by type and then listed depth-first from the systems components trees.


Previous: , Up: Files   [Contents][Index]

3.1 Lisp


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.1 trivialib.bdd.asd

Location

/home/quickref/quicklisp/dists/quicklisp/software/trivialib.bdd-20180328-git/trivialib.bdd.asd

Systems

trivialib.bdd (system)


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.2 trivialib.bdd/0.package.lisp

Parent

trivialib.bdd (system)

Location

0.package.lisp

Packages

trivialib.bdd


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.3 trivialib.bdd/1.struct.lisp

Dependency

0.package.lisp (file)

Parent

trivialib.bdd (system)

Location

1.struct.lisp

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.4 trivialib.bdd/2.odd.lisp

Dependency

1.struct.lisp (file)

Parent

trivialib.bdd (system)

Location

2.odd.lisp

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.5 trivialib.bdd/3.bdd.lisp

Dependency

2.odd.lisp (file)

Parent

trivialib.bdd (system)

Location

3.bdd.lisp

Exported Definitions

Previous: , Up: Lisp files   [Contents][Index]

3.1.6 trivialib.bdd/4.zdd.lisp

Dependency

3.bdd.lisp (file)

Parent

trivialib.bdd (system)

Location

4.zdd.lisp

Exported Definitions

Next: , Previous: , Up: Top   [Contents][Index]

4 Packages

Packages are listed by definition order.


Previous: , Up: Packages   [Contents][Index]

4.1 trivialib.bdd

Source

0.package.lisp (file)

Use List
Exported Definitions
Internal Definitions

Next: , Previous: , Up: Top   [Contents][Index]

5 Definitions

Definitions are sorted by export status, category, package, and then by lexicographic order.


Next: , Previous: , Up: Definitions   [Contents][Index]

5.1 Exported definitions


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.1 Macros

Macro: with-odd-context (&key DEFAULT VARIABLES NODE-CACHE OPERATION &allow-other-keys) &body BODY

Execute BODY in a dynamic environment where the context variables (‘*VARIABLES*’ , ‘*NODE-CACHE*’ and ‘*OPERATION*’) are set. DEFAULT should be nil or an ODD object, in which case
the context variables are inherited by the given ODD.

Package

trivialib.bdd

Source

2.odd.lisp (file)


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.2 Functions

Function: !unit VARIABLE

Returns a BDD node whose HI node is a terminal node of NIL and LO node is a terminal node of T (opposite to UNIT). Useful for representing a boolean variable.

Package

trivialib.bdd

Source

3.bdd.lisp (file)

Function: bdd ROOT &optional VARIABLES NODE-CACHE

Shortcut for instantiating an ODD using BDD-APPLY.

Package

trivialib.bdd

Source

3.bdd.lisp (file)

Function: bdd-apply F G OP-LEAF

APPLY rule for BDD.

Package

trivialib.bdd

Source

3.bdd.lisp (file)

Function: bdd-node VARIABLE HI LO

Node generation & pruning rule for BDD.

Package

trivialib.bdd

Source

3.bdd.lisp (file)

Function: call-with-odd-context DEFAULT VARIABLES NODE-CACHE OPERATION BODY-FN

Function version of WITH-ODD-CONTEXT.

Package

trivialib.bdd

Source

2.odd.lisp (file)

Function: change F VARIABLE

Change operation defined in MINATO et al. 93’. Flip the existense of a given variable in the family of sets. Examples:
(change {{1,3} {2,5}} 6) –> {{1,3,6} {2,5,6}}
(change {{1,3} {2,5,6}} 6) –> {{1,3,6} {2,5}}

Package

trivialib.bdd

Source

4.zdd.lisp (file)

Function: leaf THING

Return the leaf node in the hash table *leaf-cache*, creating an instance when required

Package

trivialib.bdd

Source

1.struct.lisp (file)

Function: make-family FAMILIES

Example: (make-family ’((1 3 5) (2 4))) –> a zdd representing {{1,3,5},{2,4}}

Package

trivialib.bdd

Source

4.zdd.lisp (file)

Function: make-set VARIABLES

Example: (make-set ’(1 3 5)) –> a zdd representing {{1,3,5}}

Package

trivialib.bdd

Source

4.zdd.lisp (file)

Function: odd &optional ROOT VARIABLES NODE-CACHE OPERATION
Package

trivialib.bdd

Source

2.odd.lisp (file)

Function: odd-apply ODD1 ODD2 LEAF-OPERATION

Applies the operation stored in ODD, recursively. At the leaf-level, applies LEAF-OPERATION.

Package

trivialib.bdd

Source

2.odd.lisp (file)

Function: unit VARIABLE

Returns a BDD node whose HI node is a terminal node of T and LO node is a terminal node of NIL. Useful for representing a boolean variable.

Package

trivialib.bdd

Source

3.bdd.lisp (file)

Function: zdd ROOT &optional VARIABLES NODE-CACHE

Shortcut for instantiating an ODD using ZDD-APPLY.

Package

trivialib.bdd

Source

4.zdd.lisp (file)

Function: zdd-apply F G OP-LEAF

APPLY rule for ZDD.

Package

trivialib.bdd

Source

4.zdd.lisp (file)

Function: zdd-node VARIABLE HI LO

Node generation & pruning rule for ZDD.

Package

trivialib.bdd

Source

4.zdd.lisp (file)


Previous: , Up: Exported definitions   [Contents][Index]

5.1.3 Structures

Structure: leaf ()

Leaf node of a decision diagram

Package

trivialib.bdd

Source

1.struct.lisp (file)

Direct superclasses

structure-object (structure)

Direct slots
Slot: content
Readers

leaf-content (function)

Writers

(setf leaf-content) (function)

Structure: node ()

lightweight node in Decision Diagram.
VARIABLE: an integer representing the index of a variable. cf. VARIABLES slot in structure DD HI,LO: hi/lo pointer

Package

trivialib.bdd

Source

1.struct.lisp (file)

Direct superclasses

structure-object (structure)

Direct slots
Slot: variable
Type

fixnum

Initform

0

Readers

node-variable (function)

Writers

(setf node-variable) (function)

Slot: hi
Type

(or trivialib.bdd:node trivialib.bdd:leaf)

Initform

(trivialib.bdd:leaf nil)

Readers

node-hi (function)

Writers

(setf node-hi) (function)

Slot: lo
Type

(or trivialib.bdd:node trivialib.bdd:leaf)

Initform

(trivialib.bdd:leaf nil)

Readers

node-lo (function)

Writers

(setf node-lo) (function)

Structure: odd ()

Structure representing a whole Decision Diagram.
Holds the context information such as variables and node-cache. For different variable ordering, ODDs are incompatible.

Package

trivialib.bdd

Source

2.odd.lisp (file)

Direct superclasses

structure-object (structure)

Direct slots
Slot: root
Type

(or trivialib.bdd:node trivialib.bdd:leaf)

Initform

(trivialib.bdd:leaf nil)

Readers

odd-root (function)

Writers

(setf odd-root) (function)

Slot: variables
Type

sequence

Initform

trivialib.bdd::*variables*

Readers

odd-variables (function)

Writers

(setf odd-variables) (function)

Slot: node-cache
Type

hash-table

Initform

trivialib.bdd::*node-cache*

Readers

odd-node-cache (function)

Writers

(setf odd-node-cache) (function)

Slot: operation
Type

(function ((or trivialib.bdd:node trivialib.bdd:leaf) (or trivialib.bdd:node trivialib.bdd:leaf) (function (* *) *)) (or trivialib.bdd:node trivialib.bdd:leaf))

Initform

trivialib.bdd::*operation*

Readers

odd-operation (function)

Writers

(setf odd-operation) (function)


Previous: , Up: Definitions   [Contents][Index]

5.2 Internal definitions


Next: , Previous: , Up: Internal definitions   [Contents][Index]

5.2.1 Special variables

Special Variable: *leaf-cache*

hash table to look up a leaf node of a thing.

Package

trivialib.bdd

Source

1.struct.lisp (file)

Special Variable: *node-cache*

Hash table to look up in order to avoid the creation of redundunt nodes.
This cache is specific to the ODD context defined by the pair of variables and operation(BDD-APPLY or ZDD-APPLY).

Package

trivialib.bdd

Source

1.struct.lisp (file)

Special Variable: *operation*

Generic operations for a decision diagram in the current context, either #’BDD-APPLY or #’ZDD-APPLY.

Package

trivialib.bdd

Source

2.odd.lisp (file)

Special Variable: *variables*

ODD variables in the current context.

Package

trivialib.bdd

Source

1.struct.lisp (file)


Previous: , Up: Internal definitions   [Contents][Index]

5.2.2 Functions

Function: copy-leaf INSTANCE
Package

trivialib.bdd

Source

1.struct.lisp (file)

Function: copy-node INSTANCE
Package

trivialib.bdd

Source

1.struct.lisp (file)

Function: copy-odd INSTANCE
Package

trivialib.bdd

Source

2.odd.lisp (file)

Function: leaf-content INSTANCE
Function: (setf leaf-content) VALUE INSTANCE
Package

trivialib.bdd

Source

1.struct.lisp (file)

Function: leaf-p OBJECT
Package

trivialib.bdd

Source

1.struct.lisp (file)

Function: make-leaf &key (CONTENT CONTENT)
Package

trivialib.bdd

Source

1.struct.lisp (file)

Function: make-node &key (VARIABLE VARIABLE) (HI HI) (LO LO)
Package

trivialib.bdd

Source

1.struct.lisp (file)

Function: make-odd &key ROOT VARIABLES NODE-CACHE OPERATION
Package

trivialib.bdd

Source

2.odd.lisp (file)

Function: node-hi INSTANCE
Function: (setf node-hi) VALUE INSTANCE
Package

trivialib.bdd

Source

1.struct.lisp (file)

Function: node-lo INSTANCE
Function: (setf node-lo) VALUE INSTANCE
Package

trivialib.bdd

Source

1.struct.lisp (file)

Function: node-p OBJECT
Package

trivialib.bdd

Source

1.struct.lisp (file)

Function: node-variable INSTANCE
Function: (setf node-variable) VALUE INSTANCE
Package

trivialib.bdd

Source

1.struct.lisp (file)

Function: odd-compatible-p ODD1 ODD2

Check if two ODDs have the same variable ordering, node-cache, and operations.

Package

trivialib.bdd

Source

2.odd.lisp (file)

Function: odd-node-cache INSTANCE
Package

trivialib.bdd

Source

2.odd.lisp (file)

Function: odd-operation INSTANCE
Package

trivialib.bdd

Source

2.odd.lisp (file)

Function: odd-p OBJECT
Package

trivialib.bdd

Source

2.odd.lisp (file)

Function: odd-root INSTANCE
Package

trivialib.bdd

Source

2.odd.lisp (file)

Function: odd-variables INSTANCE
Package

trivialib.bdd

Source

2.odd.lisp (file)


Previous: , Up: Top   [Contents][Index]

Appendix A Indexes


Next: , Previous: , Up: Indexes   [Contents][Index]

A.1 Concepts

Jump to:   F   L   T  
Index Entry  Section

F
File, Lisp, trivialib.bdd.asd: The trivialib<dot>bdd<dot>asd file
File, Lisp, trivialib.bdd/0.package.lisp: The trivialib<dot>bdd/0<dot>package<dot>lisp file
File, Lisp, trivialib.bdd/1.struct.lisp: The trivialib<dot>bdd/1<dot>struct<dot>lisp file
File, Lisp, trivialib.bdd/2.odd.lisp: The trivialib<dot>bdd/2<dot>odd<dot>lisp file
File, Lisp, trivialib.bdd/3.bdd.lisp: The trivialib<dot>bdd/3<dot>bdd<dot>lisp file
File, Lisp, trivialib.bdd/4.zdd.lisp: The trivialib<dot>bdd/4<dot>zdd<dot>lisp file

L
Lisp File, trivialib.bdd.asd: The trivialib<dot>bdd<dot>asd file
Lisp File, trivialib.bdd/0.package.lisp: The trivialib<dot>bdd/0<dot>package<dot>lisp file
Lisp File, trivialib.bdd/1.struct.lisp: The trivialib<dot>bdd/1<dot>struct<dot>lisp file
Lisp File, trivialib.bdd/2.odd.lisp: The trivialib<dot>bdd/2<dot>odd<dot>lisp file
Lisp File, trivialib.bdd/3.bdd.lisp: The trivialib<dot>bdd/3<dot>bdd<dot>lisp file
Lisp File, trivialib.bdd/4.zdd.lisp: The trivialib<dot>bdd/4<dot>zdd<dot>lisp file

T
trivialib.bdd.asd: The trivialib<dot>bdd<dot>asd file
trivialib.bdd/0.package.lisp: The trivialib<dot>bdd/0<dot>package<dot>lisp file
trivialib.bdd/1.struct.lisp: The trivialib<dot>bdd/1<dot>struct<dot>lisp file
trivialib.bdd/2.odd.lisp: The trivialib<dot>bdd/2<dot>odd<dot>lisp file
trivialib.bdd/3.bdd.lisp: The trivialib<dot>bdd/3<dot>bdd<dot>lisp file
trivialib.bdd/4.zdd.lisp: The trivialib<dot>bdd/4<dot>zdd<dot>lisp file

Jump to:   F   L   T  

Next: , Previous: , Up: Indexes   [Contents][Index]

A.2 Functions

Jump to:   !   (  
B   C   F   L   M   N   O   U   W   Z  
Index Entry  Section

!
!unit: Exported functions

(
(setf leaf-content): Internal functions
(setf node-hi): Internal functions
(setf node-lo): Internal functions
(setf node-variable): Internal functions

B
bdd: Exported functions
bdd-apply: Exported functions
bdd-node: Exported functions

C
call-with-odd-context: Exported functions
change: Exported functions
copy-leaf: Internal functions
copy-node: Internal functions
copy-odd: Internal functions

F
Function, !unit: Exported functions
Function, (setf leaf-content): Internal functions
Function, (setf node-hi): Internal functions
Function, (setf node-lo): Internal functions
Function, (setf node-variable): Internal functions
Function, bdd: Exported functions
Function, bdd-apply: Exported functions
Function, bdd-node: Exported functions
Function, call-with-odd-context: Exported functions
Function, change: Exported functions
Function, copy-leaf: Internal functions
Function, copy-node: Internal functions
Function, copy-odd: Internal functions
Function, leaf: Exported functions
Function, leaf-content: Internal functions
Function, leaf-p: Internal functions
Function, make-family: Exported functions
Function, make-leaf: Internal functions
Function, make-node: Internal functions
Function, make-odd: Internal functions
Function, make-set: Exported functions
Function, node-hi: Internal functions
Function, node-lo: Internal functions
Function, node-p: Internal functions
Function, node-variable: Internal functions
Function, odd: Exported functions
Function, odd-apply: Exported functions
Function, odd-compatible-p: Internal functions
Function, odd-node-cache: Internal functions
Function, odd-operation: Internal functions
Function, odd-p: Internal functions
Function, odd-root: Internal functions
Function, odd-variables: Internal functions
Function, unit: Exported functions
Function, zdd: Exported functions
Function, zdd-apply: Exported functions
Function, zdd-node: Exported functions

L
leaf: Exported functions
leaf-content: Internal functions
leaf-p: Internal functions

M
Macro, with-odd-context: Exported macros
make-family: Exported functions
make-leaf: Internal functions
make-node: Internal functions
make-odd: Internal functions
make-set: Exported functions

N
node-hi: Internal functions
node-lo: Internal functions
node-p: Internal functions
node-variable: Internal functions

O
odd: Exported functions
odd-apply: Exported functions
odd-compatible-p: Internal functions
odd-node-cache: Internal functions
odd-operation: Internal functions
odd-p: Internal functions
odd-root: Internal functions
odd-variables: Internal functions

U
unit: Exported functions

W
with-odd-context: Exported macros

Z
zdd: Exported functions
zdd-apply: Exported functions
zdd-node: Exported functions

Jump to:   !   (  
B   C   F   L   M   N   O   U   W   Z  

Next: , Previous: , Up: Indexes   [Contents][Index]

A.3 Variables

Jump to:   *  
C   H   L   N   O   R   S   V  
Index Entry  Section

*
*leaf-cache*: Internal special variables
*node-cache*: Internal special variables
*operation*: Internal special variables
*variables*: Internal special variables

C
content: Exported structures

H
hi: Exported structures

L
lo: Exported structures

N
node-cache: Exported structures

O
operation: Exported structures

R
root: Exported structures

S
Slot, content: Exported structures
Slot, hi: Exported structures
Slot, lo: Exported structures
Slot, node-cache: Exported structures
Slot, operation: Exported structures
Slot, root: Exported structures
Slot, variable: Exported structures
Slot, variables: Exported structures
Special Variable, *leaf-cache*: Internal special variables
Special Variable, *node-cache*: Internal special variables
Special Variable, *operation*: Internal special variables
Special Variable, *variables*: Internal special variables

V
variable: Exported structures
variables: Exported structures

Jump to:   *  
C   H   L   N   O   R   S   V  

Previous: , Up: Indexes   [Contents][Index]

A.4 Data types

Jump to:   L   N   O   P   S   T  
Index Entry  Section

L
leaf: Exported structures

N
node: Exported structures

O
odd: Exported structures

P
Package, trivialib.bdd: The trivialib<dot>bdd package

S
Structure, leaf: Exported structures
Structure, node: Exported structures
Structure, odd: Exported structures
System, trivialib.bdd: The trivialib<dot>bdd system

T
trivialib.bdd: The trivialib<dot>bdd system
trivialib.bdd: The trivialib<dot>bdd package

Jump to:   L   N   O   P   S   T