8eace5aaf113

Get some basic ZDD stuff up and running with triviabdd
[view raw] [browse files]
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)))))))