The trivialib.bdd Reference Manual

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 4.0 beta 2 "William Riker" on Mon Aug 15 06:05:03 2022 GMT+0.

Table of Contents


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.





2 Systems

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


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

2.1 trivialib.bdd

BDD and ZDD implementation using Trivia

Author

Masataro Asai

Contact

guicho2.71828@gmail.com

License

LLGPL

Version

0.1

Dependencies
  • alexandria (system).
  • trivia (system).
  • trivial-garbage (system).
  • immutable-struct (system).
Source

trivialib.bdd.asd.

Child Components

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   [Contents][Index]

3.1.1 trivialib.bdd/trivialib.bdd.asd

Source

trivialib.bdd.asd.

Parent Component

trivialib.bdd (system).

ASDF Systems

trivialib.bdd.


3.1.2 trivialib.bdd/0.package.lisp

Source

trivialib.bdd.asd.

Parent Component

trivialib.bdd (system).

Packages

trivialib.bdd.


3.1.3 trivialib.bdd/1.struct.lisp

Dependency

0.package.lisp (file).

Source

trivialib.bdd.asd.

Parent Component

trivialib.bdd (system).

Public Interface
Internals

3.1.4 trivialib.bdd/2.odd.lisp

Dependency

1.struct.lisp (file).

Source

trivialib.bdd.asd.

Parent Component

trivialib.bdd (system).

Public Interface
Internals

3.1.5 trivialib.bdd/3.bdd.lisp

Dependency

2.odd.lisp (file).

Source

trivialib.bdd.asd.

Parent Component

trivialib.bdd (system).

Public Interface

3.1.6 trivialib.bdd/4.zdd.lisp

Dependency

3.bdd.lisp (file).

Source

trivialib.bdd.asd.

Parent Component

trivialib.bdd (system).

Public Interface

4 Packages

Packages are listed by definition order.


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

4.1 trivialib.bdd

Source

0.package.lisp.

Use List
  • alexandria.
  • common-lisp.
  • trivia.level2.
Public Interface
Internals

5 Definitions

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


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

5.1 Public Interface


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.


Next: , Previous: , Up: Public Interface   [Contents][Index]

5.1.2 Ordinary 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.

Function: bdd (root &optional variables node-cache)

Shortcut for instantiating an ODD using BDD-APPLY.

Package

trivialib.bdd.

Source

3.bdd.lisp.

Function: bdd-apply (f g op-leaf)

APPLY rule for BDD.

Package

trivialib.bdd.

Source

3.bdd.lisp.

Function: bdd-node (variable hi lo)

Node generation & pruning rule for BDD.

Package

trivialib.bdd.

Source

3.bdd.lisp.

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.

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.

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.

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.

Function: make-set (variables)

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

Package

trivialib.bdd.

Source

4.zdd.lisp.

Function: odd (&optional root variables node-cache operation)
Package

trivialib.bdd.

Source

2.odd.lisp.

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.

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.

Function: zdd (root &optional variables node-cache)

Shortcut for instantiating an ODD using ZDD-APPLY.

Package

trivialib.bdd.

Source

4.zdd.lisp.

Function: zdd-apply (f g op-leaf)

APPLY rule for ZDD.

Package

trivialib.bdd.

Source

4.zdd.lisp.

Function: zdd-node (variable hi lo)

Node generation & pruning rule for ZDD.

Package

trivialib.bdd.

Source

4.zdd.lisp.


5.1.3 Structures

Structure: leaf

Leaf node of a decision diagram

Package

trivialib.bdd.

Source

1.struct.lisp.

Direct superclasses

structure-object.

Direct slots
Slot: content
Readers

leaf-content.

Writers

(setf leaf-content).

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.

Direct superclasses

structure-object.

Direct slots
Slot: variable
Package

common-lisp.

Type

fixnum

Initform

0

Readers

node-variable.

Writers

(setf node-variable).

Slot: hi
Type

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

Initform

(trivialib.bdd:leaf nil)

Readers

node-hi.

Writers

(setf node-hi).

Slot: lo
Type

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

Initform

(trivialib.bdd:leaf nil)

Readers

node-lo.

Writers

(setf node-lo).

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.

Direct superclasses

structure-object.

Direct slots
Slot: root
Package

none (uninterned).

Type

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

Initform

(trivialib.bdd:leaf nil)

Readers

odd-root.

Writers

This slot is read-only.

Slot: variables
Package

none (uninterned).

Type

sequence

Initform

trivialib.bdd::*variables*

Readers

odd-variables.

Writers

This slot is read-only.

Slot: node-cache
Package

none (uninterned).

Type

hash-table

Initform

trivialib.bdd::*node-cache*

Readers

odd-node-cache.

Writers

This slot is read-only.

Slot: operation
Package

none (uninterned).

Type

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

Initform

trivialib.bdd::*operation*

Readers

odd-operation.

Writers

This slot is read-only.


5.2 Internals


Next: , Previous: , Up: Internals   [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.

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.

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.

Special Variable: *variables*

ODD variables in the current context.

Package

trivialib.bdd.

Source

1.struct.lisp.


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

5.2.2 Ordinary functions

Function: copy-leaf (instance)
Package

trivialib.bdd.

Source

1.struct.lisp.

Function: copy-node (instance)
Package

trivialib.bdd.

Source

1.struct.lisp.

Function: copy-odd (instance)
Package

trivialib.bdd.

Source

2.odd.lisp.

Reader: leaf-content (instance)
Writer: (setf leaf-content) (instance)
Package

trivialib.bdd.

Source

1.struct.lisp.

Target Slot

content.

Function: leaf-p (object)
Package

trivialib.bdd.

Source

1.struct.lisp.

Function: make-leaf (&key content)
Package

trivialib.bdd.

Source

1.struct.lisp.

Function: make-node (&key variable hi lo)
Package

trivialib.bdd.

Source

1.struct.lisp.

Function: make-odd (&key root variables node-cache operation)
Package

trivialib.bdd.

Source

2.odd.lisp.

Reader: node-hi (instance)
Writer: (setf node-hi) (instance)
Package

trivialib.bdd.

Source

1.struct.lisp.

Target Slot

hi.

Reader: node-lo (instance)
Writer: (setf node-lo) (instance)
Package

trivialib.bdd.

Source

1.struct.lisp.

Target Slot

lo.

Function: node-p (object)
Package

trivialib.bdd.

Source

1.struct.lisp.

Reader: node-variable (instance)
Writer: (setf node-variable) (instance)
Package

trivialib.bdd.

Source

1.struct.lisp.

Target Slot

variable.

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.

Reader: odd-node-cache (instance)
Package

trivialib.bdd.

Source

2.odd.lisp.

Target Slot

node-cache.

Reader: odd-operation (instance)
Package

trivialib.bdd.

Source

2.odd.lisp.

Target Slot

operation.

Function: odd-p (object)
Package

trivialib.bdd.

Source

2.odd.lisp.

Reader: odd-root (instance)
Package

trivialib.bdd.

Source

2.odd.lisp.

Target Slot

root.

Reader: odd-variables (instance)
Package

trivialib.bdd.

Source

2.odd.lisp.

Target Slot

variables.


Appendix A Indexes


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

A.1 Concepts


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: Public ordinary functions

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

B
bdd: Public ordinary functions
bdd-apply: Public ordinary functions
bdd-node: Public ordinary functions

C
call-with-odd-context: Public ordinary functions
change: Public ordinary functions
copy-leaf: Private ordinary functions
copy-node: Private ordinary functions
copy-odd: Private ordinary functions

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

L
leaf: Public ordinary functions
leaf-content: Private ordinary functions
leaf-p: Private ordinary functions

M
Macro, with-odd-context: Public macros
make-family: Public ordinary functions
make-leaf: Private ordinary functions
make-node: Private ordinary functions
make-odd: Private ordinary functions
make-set: Public ordinary functions

N
node-hi: Private ordinary functions
node-lo: Private ordinary functions
node-p: Private ordinary functions
node-variable: Private ordinary functions

O
odd: Public ordinary functions
odd-apply: Public ordinary functions
odd-compatible-p: Private ordinary functions
odd-node-cache: Private ordinary functions
odd-operation: Private ordinary functions
odd-p: Private ordinary functions
odd-root: Private ordinary functions
odd-variables: Private ordinary functions

U
unit: Public ordinary functions

W
with-odd-context: Public macros

Z
zdd: Public ordinary functions
zdd-apply: Public ordinary functions
zdd-node: Public ordinary functions

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