# HG changeset patch # User Steve Losh # Date 1471803263 0 # Node ID 7eb23163afcfa2d5fa7d4e474ea325330a11bbbb # Parent b5708cf443c2eaa3cb78d049360fd0af6f6703a3 Use cl-adt to massively simplify BDDs diff -r b5708cf443c2 -r 7eb23163afcf sand.asd --- 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 diff -r b5708cf443c2 -r 7eb23163afcf src/binary-decision-diagrams.lisp --- 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)