# HG changeset patch # User Steve Losh # Date 1477758846 0 # Node ID 8eace5aaf113b25072ea0fc1a69039cb6936d45e # Parent 0306f46e89fb2fafc7c74b7c9d6b8fbf8e16712e Get some basic ZDD stuff up and running with triviabdd diff -r 0306f46e89fb -r 8eace5aaf113 package.lisp --- 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) diff -r 0306f46e89fb -r 8eace5aaf113 src/zdd.lisp --- 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)))))))