Use cl-adt to massively simplify BDDs
author |
Steve Losh <steve@stevelosh.com> |
date |
Sun, 21 Aug 2016 18:14:23 +0000 |
parents |
b5708cf443c2
|
children |
1d59a2656cfc
|
branches/tags |
(none) |
files |
sand.asd src/binary-decision-diagrams.lisp |
Changes
--- a/sand.asd Sun Aug 21 17:52:19 2016 +0000
+++ b/sand.asd Sun Aug 21 18:14:23 2016 +0000
@@ -22,6 +22,7 @@
#:html-entities
#:plump
#:clss
+ #:cl-algebraic-data-type
)
:serial t
--- a/src/binary-decision-diagrams.lisp Sun Aug 21 17:52:19 2016 +0000
+++ b/src/binary-decision-diagrams.lisp Sun Aug 21 18:14:23 2016 +0000
@@ -1,35 +1,20 @@
(in-package #:sand.binary-decision-diagrams)
+(deftype non-negative-fixnum ()
+ `(integer 0 ,most-positive-fixnum))
+
-(defun required ()
- (error "Argument required."))
-
-
-(defstruct (bdd (:constructor %make-bdd (number low high)))
- (number (required) :type fixnum)
- (low (required) :type (or bit bdd))
- (high (required) :type (or bit bdd)))
+;;;; Reference ----------------------------------------------------------------
+(adt:defdata bdd
+ (sink bit)
+ (node non-negative-fixnum bdd bdd))
(defun make-bdd (contents)
(etypecase contents
- (bit contents)
+ (bit (sink contents))
(cons
(destructuring-bind (number low high) contents
- (%make-bdd number (make-bdd low) (make-bdd high))))))
-
-(defmacro bdd-case (bdd
- ((sink) &body sink-body)
- ((number low high) &body node-body))
- (once-only (bdd)
- `(etypecase ,bdd
- (bit (let ((,sink ,bdd))
- (declare (ignorable ,sink))
- ,@sink-body))
- (bdd (with-accessors ((,number bdd-number)
- (,low bdd-low)
- (,high bdd-high))
- ,bdd
- ,@node-body)))))
+ (node number (make-bdd low) (make-bdd high))))))
(defun evaluate-bdd (bdd &rest arguments)
@@ -37,35 +22,35 @@
(bdd bdd)
(argument (first arguments))
(remaining (rest arguments)))
- (bdd-case bdd
- ((sink) sink)
- ((number low high)
+ (adt:match bdd bdd
+ ((sink bit) bit)
+ ((node number low high)
(if (> number n)
- (recur (1+ n)
- bdd
- argument
- remaining)
- (recur (1+ n)
- (if (zerop argument)
- low
- high)
- (first remaining)
- (rest remaining)))))))
+ (recur (1+ n)
+ bdd
+ argument
+ remaining)
+ (recur (1+ n)
+ (if (zerop argument)
+ low
+ high)
+ (first remaining)
+ (rest remaining)))))))
(defun bdd-map-nodes (function bdd)
- (bdd-case bdd
- ((sink)
- (list (funcall function sink)))
- ((n low high)
+ (adt:match bdd bdd
+ ((sink _)
+ (list (funcall function bdd)))
+ ((node _ low high)
(append (list (funcall function bdd))
(bdd-map-nodes function low)
(bdd-map-nodes function high)))))
(defun bdd-map-edges (function bdd)
- (bdd-case bdd
- ((sink) nil)
- ((n low high)
+ (adt:match bdd bdd
+ ((sink _) nil)
+ ((node _ low high)
(list* (funcall function bdd low t)
(funcall function bdd high nil)
(append (bdd-map-edges function low)
@@ -73,14 +58,14 @@
(defun node-label (node)
- (bdd-case node
- ((sink) (if (zerop sink) 'false 'true))
- ((number low high) number)))
+ (adt:match bdd node
+ ((sink bit) (if (zerop bit) 'false 'true))
+ ((node number _ _) number)))
(defun node-shape (node)
- (bdd-case node
- ((sink) :box)
- ((n l h) :circle)))
+ (adt:match bdd node
+ ((sink _) :box)
+ ((node _ _ _) :circle)))
(defun draw-bdd (bdd &optional (path "bdd.dot"))
@@ -99,10 +84,13 @@
:path path)))
+;;;; Scratch ------------------------------------------------------------------
(defparameter *maj*
(make-bdd '(1
(2 0 (3 0 1))
(2 (3 0 1) 1))))
-(draw-bdd *maj*)
+(evaluate-bdd *maj* 1 0 1)
+
+(draw-bdd *maj* t)