--- a/package.lisp Sat Oct 29 14:48:36 2016 +0000
+++ b/package.lisp Sat Oct 29 14:48:46 2016 +0000
@@ -20,6 +20,8 @@
:scully.quickutils)
(:export))
+(defpackage :scully.cudd)
+
(defpackage :scully.zdd
(:use
:cl
@@ -27,8 +29,12 @@
:iterate
:cl-arrows
:cffi
+ ; :scully.cudd
+ :trivialib.bdd
:scully.quickutils)
- (:export))
+ (:export)
+ (:shadowing-import-from :trivialib.bdd :make-set)
+ )
(defpackage :scully.reasoners.prolog
(:use
--- a/scully.asd Sat Oct 29 14:48:36 2016 +0000
+++ b/scully.asd Sat Oct 29 14:48:46 2016 +0000
@@ -17,6 +17,7 @@
:cl-algebraic-data-type
:cl-arrows
:cl-ggp
+ :trivialib.bdd
:cffi)
:serial t
--- a/src/cudd.i Sat Oct 29 14:48:36 2016 +0000
+++ b/src/cudd.i Sat Oct 29 14:48:46 2016 +0000
@@ -5,7 +5,6 @@
%insert("lisphead")%{
-(cl:defpackage :scully.cudd)
(cl:in-package :scully.cudd)
(cffi:define-foreign-library scully.zdd::cudd
--- a/src/cudd.lisp Sat Oct 29 14:48:36 2016 +0000
+++ b/src/cudd.lisp Sat Oct 29 14:48:46 2016 +0000
@@ -5,10 +5,6 @@
;;; the SWIG interface file instead.
-(cl:when (cl:not (cl:find-package :scully.cudd))
- (cl:defpackage :scully.cudd))
-
-(cl:defpackage :scully.cudd)
(cl:in-package :scully.cudd)
(cffi:define-foreign-library scully.zdd::cudd
--- a/src/zdd.lisp Sat Oct 29 14:48:36 2016 +0000
+++ b/src/zdd.lisp Sat Oct 29 14:48:46 2016 +0000
@@ -1,10 +1,121 @@
(in-package :scully.zdd)
+; (defctype dd-halfword :uint32)
+
+; (defcstruct dd-children
+; (true :pointer)
+; (else :pointer))
+
+; (defcunion dd-node-guts
+; (value :double)
+; (kids (:struct dd-children)))
+
+; (defcstruct dd-node
+; (index dd-halfword)
+; (ref dd-halfword)
+; (next (:pointer (:struct dd-node)))
+; (type (:union dd-node-guts)))
+
+
+; (defparameter *m*
+; (cudd-init 0
+; 0
+; scully.cudd:+cudd-unique-slots+
+; scully.cudd:+cudd-cache-slots+
+; 0))
+
+; (defun ref (node)
+; (cudd-ref node)
+; node)
+
+; (defun deref (&rest nodes)
+; (iterate (for node :in nodes)
+; (cudd-recursive-deref-zdd *m* node))
+; (values))
+
+; (defun var (index)
+; (let ((node (cudd-zdd-ith-var *m* index)))
+; (ref node)
+; node))
+
+; (defun draw (node &optional (filename "zdd.dot"))
+; (format t "Cover~%")
+; (cudd-zdd-print-cover *m* node)
+; (format t "~%Node Count: ~A~%"
+; (cudd-zdd-read-node-count *m*))
+; (format t "~%Minterm~%")
+; (cudd-zdd-print-minterm *m* node)
+; (format t "~%Debug~%")
+; (cudd-zdd-print-debug *m* node 0 10)
+; (format t "~%Table~%")
+; (cudd-zdd-print-subtable *m*)
+; (let ((file (foreign-funcall "fopen" :string filename :string "w" :pointer)))
+; (unwind-protect
+; (let ((node-array (foreign-alloc :pointer :initial-element node)))
+; (cudd-zdd-dump-dot *m* 1 node-array (null-pointer) (null-pointer) file)
+; (foreign-free node-array))
+; (foreign-funcall "fclose" :pointer file))))
+
-(defparameter *cudd-manager*
- (scully.cudd:cudd-init 0
- 0
- scully.cudd:+cudd-unique-slots+
- scully.cudd:+cudd-cache-slots+
- 0))
+; (defun test ()
+; (let* ((a (var 0))
+; (b (var 1))
+; (result (ref (cudd-zdd-union *m* a b))))
+; (deref a b)
+; (draw result)
+; (deref result)))
+
+; (defun test ()
+; (let* ((a (var 1)))
+; (draw a)
+; (deref a)))
+
+; (test)
+; (draw (cudd-zdd-ith-var *m* 0))
+
+; (draw (cudd-read-zdd-one *m* 0))
+
+; (draw (cudd-read-zero *m*))
+; (test)
+
+
+(defun gcprint (thing &rest args)
+ (let ((*print-circle* t))
+ (apply #'print
+ (prog1 thing
+ (tg:gc :full t :verbose t))
+ args)))
+
+(setf cl-dot:*dot-path* "/usr/local/bin/dot")
+(defmethod attrs (object &rest attributes)
+ (make-instance 'cl-dot:attributed
+ :object object
+ :attributes attributes))
+
+(defmethod cl-dot:graph-object-node ((graph (eql 'zdd))
+ (object leaf))
+ (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)))
+
+(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)))
+
+(defun draw (zdd &optional (filename "zdd.png"))
+ (cl-dot:dot-graph
+ (cl-dot:generate-graph-from-roots 'zdd (list zdd))
+ filename
+ :format :png))
+
+
+(with-odd-context (:operation #'zdd-apply)
+ (draw (gcprint (make-family '((4) ())))))