7eb23163afcf

Use cl-adt to massively simplify BDDs
[view raw] [browse files]
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)