Get some basic ZDD stuff up and running with triviabdd
author |
Steve Losh <steve@stevelosh.com> |
date |
Sat, 29 Oct 2016 16:34:06 +0000 |
parents |
0306f46e89fb
|
children |
ecd4aaf2cc10
|
branches/tags |
(none) |
files |
package.lisp src/zdd.lisp |
Changes
--- a/package.lisp Sat Oct 29 14:50:01 2016 +0000
+++ b/package.lisp Sat Oct 29 16:34:06 2016 +0000
@@ -20,13 +20,13 @@
:scully.quickutils)
(:export))
-
(defpackage :scully.zdd
(:use
:cl
:losh
:iterate
:cl-arrows
+ :trivia
:trivialib.bdd
:scully.quickutils)
(:export)
--- a/src/zdd.lisp Sat Oct 29 14:50:01 2016 +0000
+++ b/src/zdd.lisp Sat Oct 29 16:34:06 2016 +0000
@@ -1,5 +1,10 @@
(in-package :scully.zdd)
+(defpattern leaf (&optional content)
+ `(structure leaf :content ,content))
+
+
+;;;; Utils --------------------------------------------------------------------
(defun gcprint (thing &rest args)
(let ((*print-circle* t))
(apply #'print
@@ -7,36 +12,100 @@
(tg:gc :full t :verbose t))
args)))
+
+;;;; GraphViz -----------------------------------------------------------------
(setf cl-dot:*dot-path* "/usr/local/bin/dot")
-(defmethod attrs (object &rest attributes)
+(defun attrs (object &rest attributes)
(make-instance 'cl-dot:attributed
- :object object
- :attributes attributes))
+ :object object
+ :attributes attributes))
(defmethod cl-dot:graph-object-node ((graph (eql 'zdd))
- (object leaf))
+ (object t))
(make-instance 'cl-dot:node
- :attributes `(:label ,(trivialib.bdd::leaf-content object)
- :shape :ellipse)))
-
-(defmethod cl-dot:graph-object-node ((graph (eql 'zdd))
- (object node))
- (make-instance 'cl-dot:node
- :attributes `(:label ,(trivialib.bdd::node-variable object)
- :shape :box)))
+ :attributes (ematch object
+ ((leaf c) `(:label ,c :shape :ellipse))
+ ((node v) `(:label ,v :shape :box)))))
(defmethod cl-dot:graph-object-points-to ((graph (eql 'zdd))
- (object node))
- (list (attrs (trivialib.bdd::node-hi object) :style :solid)
- (attrs (trivialib.bdd::node-lo object) :style :dashed)))
+ (object t))
+ (ematch object
+ ((leaf) '())
+ ((node _ hi lo)
+ (list (attrs hi :style :solid)
+ (attrs lo :style :dashed)))))
(defun draw (zdd &optional (filename "zdd.png"))
(cl-dot:dot-graph
(cl-dot:generate-graph-from-roots 'zdd (list zdd))
filename
- :format :png))
+ :format :png)
+ zdd)
+
+
+;;;; ZDDs ---------------------------------------------------------------------
+(defparameter *cache* (tg:make-weak-hash-table :weakness :value :test #'equalp))
+
+
+(defmacro with-zdd (&body body)
+ `(with-odd-context (:operation #'zdd-apply :node-cache *cache*)
+ ,@body))
+
+(defun enumerate (zdd)
+ (ematch zdd
+ ((leaf nil) nil)
+ ((leaf t) (list nil))
+ ((node variable hi lo)
+ (append (mapcar (curry #'cons variable) (enumerate hi))
+ (enumerate lo)))))
+
+(defun unit-patch (z)
+ (ematch z
+ ((leaf t) z)
+ ((leaf nil) (leaf t))
+ ((node variable hi lo)
+ (zdd-node variable hi (unit-patch lo)))))
+
+
+(defun zdd-set (elements)
+ (make-set elements))
-(with-odd-context (:operation #'zdd-apply)
- (draw (gcprint (make-family '((4) ())))))
+(defun zdd-union (a b)
+ (ematch* (a b)
+ (((node) (leaf))
+ (zdd-union b a))
+
+ (((leaf nil) b)
+ b)
+
+ (((leaf t) b)
+ (unit-patch b))
+
+ (((node var-a hi-a lo-a)
+ (node var-b hi-b lo-b))
+ (cond
+ ((< var-a var-b)
+ (zdd-node var-a
+ hi-a
+ (zdd-union lo-a b)))
+ ((> var-a var-b)
+ (zdd-node var-b
+ hi-b
+ (zdd-union lo-b a)))
+ ((= var-a var-b)
+ (zdd-node var-a
+ (zdd-union hi-a hi-b)
+ (zdd-union lo-a lo-b)))))))
+
+
+(defun zdd-family (&rest sets)
+ (reduce #'zdd-union (mapcar #'zdd-set sets)))
+
+
+
+;;;; Scratch ------------------------------------------------------------------
+(with-zdd
+ (enumerate (gcprint (draw (zdd-union (zdd-family '(1 2 4) '(3 4))
+ (zdd-set '(1 2)))))))