# HG changeset patch
# User Steve Losh <steve@stevelosh.com>
# Date 1479742397 0
# Node ID addb56e3eb9d74e65a3975bc48934ec232dc8e13
# Parent  37e64253cccf8a27eeda880489d5356946c3a153
Move all the graphviz code into its own file

Also shove the old rule-tree attempt out of the way for now.

diff -r 37e64253cccf -r addb56e3eb9d package.lisp
--- a/package.lisp	Sun Nov 20 15:33:06 2016 +0000
+++ b/package.lisp	Mon Nov 21 15:33:17 2016 +0000
@@ -12,6 +12,16 @@
     :redump-gdl))
 
 
+(defpackage :scully.graphviz
+  (:use
+    :cl
+    :losh
+    :iterate
+    :cl-arrows
+    :trivia
+    :trivialib.bdd
+    :scully.quickutils))
+
 (defpackage :scully.dag
   (:use
     :cl
diff -r 37e64253cccf -r addb56e3eb9d scully.asd
--- a/scully.asd	Sun Nov 20 15:33:06 2016 +0000
+++ b/scully.asd	Mon Nov 21 15:33:17 2016 +0000
@@ -36,6 +36,7 @@
                              (:file "terms")
                              (:file "rule-trees")
                              (:file "zdd")
+                             (:file "graphviz")
                              (:module "reasoners" :serial t
                               :components ((:file "prolog")))
                              (:module "grounders" :serial t
diff -r 37e64253cccf -r addb56e3eb9d src/graphviz.lisp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/graphviz.lisp	Mon Nov 21 15:33:17 2016 +0000
@@ -0,0 +1,115 @@
+(in-package :scully.graphviz)
+
+(setf cl-dot:*dot-path* "/usr/local/bin/dot")
+
+;;;; Utils --------------------------------------------------------------------
+(defun attrs (object &rest attributes)
+  (make-instance 'cl-dot:attributed
+    :object object
+    :attributes attributes))
+
+
+;;;; Rule Trees ---------------------------------------------------------------
+(defmethod cl-dot:graph-object-node ((graph (eql 'rule-tree))
+                                     (object scully.rule-trees::rule-tree))
+  (make-instance 'cl-dot:node
+    :attributes (adt:match scully.rule-trees::rule-tree object
+                  ((scully.rule-trees::node term _ _)
+                   `(:label ,(aesthetic-string term)
+                     :shape :circle))
+
+                  (scully.rule-trees::bottom
+                    `(:label "⊥"
+                      :shape :square))
+
+                  ((scully.rule-trees::top term)
+                   `(:label ,(aesthetic-string term)
+                     :shape :rectangle)))))
+
+(defmethod cl-dot:graph-object-points-to ((graph (eql 'rule-tree))
+                                          (object scully.rule-trees::rule-tree))
+  (adt:match scully.rule-trees::rule-tree object
+    ((scully.rule-trees::node _ hi lo) (list (attrs hi :style :solid)
+                                             (attrs lo :style :dashed)))
+    ((scully.rule-trees::top _) nil)
+    (scully.rule-trees::bottom nil)))
+
+
+(defun draw-rule-tree (rule-tree &key (filename "rule-tree.png"))
+  (cl-dot:dot-graph
+    (cl-dot:generate-graph-from-roots 'rule-tree (list rule-tree))
+    filename
+    :format :png)
+  rule-tree)
+
+
+;;;; ZDDs ---------------------------------------------------------------------
+(defparameter *draw-unique-sinks* nil)
+(defparameter *draw-unique-nodes* nil)
+(defparameter *draw-hex-p* #'never)
+(defparameter *draw-label-fn* #'identity)
+
+
+(defun sink-attrs (val)
+  `(:label ,(if val "⊤" "⊥")
+    :shape :square
+    :style :filled
+    :fillcolor "#fafafa"
+    :color "#aaaaaa"
+    :fontsize 22
+    :width 0.05))
+
+
+(defmethod cl-dot:graph-object-node ((graph (eql 'zdd))
+                                     (object scully.zdd::node))
+  (make-instance 'cl-dot:node
+    :attributes (ematch object
+                  ((scully.zdd::node v)
+                   `(:label ,(funcall *draw-label-fn* v)
+                     :shape ,(if (funcall *draw-hex-p* v)
+                               :hexagon
+                               :rectangle))))))
+
+(defmethod cl-dot:graph-object-node ((graph (eql 'zdd))
+                                     (object cons))
+  (cl-dot:graph-object-node graph (car object)))
+
+(defmethod cl-dot:graph-object-node ((graph (eql 'zdd))
+                                     (object scully.zdd::leaf))
+  (make-instance 'cl-dot:node
+    :attributes (ematch object ((scully.zdd::sink c) (sink-attrs c)))))
+
+
+(defun wrap-node (object)
+  (ematch object
+    ((scully.zdd::sink) (if *draw-unique-sinks* object (cons object nil)))
+    ((scully.zdd::node) (if *draw-unique-nodes* object (cons object nil)))))
+
+(defmethod cl-dot:graph-object-points-to ((graph (eql 'zdd))
+                                          (object t))
+  (ematch object
+    ((cons object _)
+     (cl-dot:graph-object-points-to graph object))
+    ((scully.zdd::sink _)
+     '())
+    ((scully.zdd::node _ hi lo)
+     (list (attrs (wrap-node hi) :style :solid)
+           (attrs (wrap-node lo) :style :dashed)))))
+
+
+(defun draw-zdd (zdd &key
+                 (filename "zdd.png")
+                 (unique-sinks nil)
+                 (unique-nodes t)
+                 (hexp #'never)
+                 (label-fn #'identity))
+  (let ((*draw-unique-sinks* unique-sinks)
+        (*draw-unique-nodes* unique-nodes)
+        (*draw-hex-p* hexp)
+        (*draw-label-fn* label-fn))
+    (cl-dot:dot-graph
+      (cl-dot:generate-graph-from-roots 'zdd (list (wrap-node zdd)))
+      filename
+      :format :png))
+  zdd)
+
diff -r 37e64253cccf -r addb56e3eb9d src/old-rule-trees.lisp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/old-rule-trees.lisp	Mon Nov 21 15:33:17 2016 +0000
@@ -0,0 +1,149 @@
+;;;; Rule Trees ---------------------------------------------------------------
+(defun rule-head (rule)
+  (first rule))
+
+(defun rule-body (rule)
+  (rest rule))
+
+(defun rule-first-body (rule)
+  (first (rule-body rule)))
+
+(defun rule-empty-p (rule)
+  (null (rule-body rule)))
+
+
+(defun negationp (term)
+  (and (consp term) (eql 'ggp-rules::not (first term))))
+
+(defun bare-term (term)
+  (if (negationp term)
+    (second term)
+    term))
+
+(defun term< (t1 t2)
+  (< (bare-term t1) (bare-term t2)))
+
+
+(defun sort-body (rule)
+  (destructuring-bind (head . body) rule
+    (list* head (sort body #'term<))))
+
+(defun drop-first (rule)
+  (destructuring-bind (head . body) rule
+    (list* head (rest body))))
+
+(defun find-smallest-body-term (rules)
+  (-<> rules
+    (mapcar #'rule-first-body <>)
+    (sort <> #'term<)
+    (first <>)))
+
+(defun partition-rules (rules)
+  (let ((element (bare-term (find-smallest-body-term rules))))
+    (labels
+        ((rule-requires (rule)
+           (equal (rule-first-body rule) element))
+         (rule-disallows (rule)
+           (equal (rule-first-body rule) `(ggp-rules::not ,element)))
+         (rule-ignores (rule)
+           (not (or (rule-requires rule)
+                    (rule-disallows rule)))))
+      (values element
+              (remove-if-not #'rule-disallows rules)
+              (remove-if-not #'rule-requires rules)
+              (remove-if-not #'rule-ignores rules)))))
+
+
+(defmethod print-object ((set hash-set) stream)
+  (print-unreadable-object (set stream :type t :identity nil)
+    (prin1 (set->list set) stream)))
+
+(defun hash-set= (s1 s2)
+  (zerop (set-size (set-symmetric-diff s1 s2))))
+
+(defun rule-head-in (set rule)
+  (set-lookup set (rule-head rule)))
+
+(defun collapse-positive-heads (rules-and-heads)
+  (destructuring-bind (rules heads) rules-and-heads
+    (flet ((update-rule (rule)
+             (cons (rule-head rule)
+                   (remove-if (curry #'set-lookup heads)
+                              (rule-body rule)))))
+      (let* ((new-rules (set-map #'update-rule rules))
+             (new-heads (-<> new-rules
+                          (set-filter #'rule-empty-p <>)
+                          (set-map #'rule-head <>))))
+        (list (set-filter (complement (curry #'rule-head-in new-heads))
+                          new-rules)
+              (set-union heads new-heads))))))
+
+(defun find-strictly-negative-rules (rules)
+  (set-filter (lambda (rule)
+                (every #'negationp (rule-body rule)))
+              rules))
+
+(defun collapse-negative-heads (rules-and-heads)
+  (destructuring-bind (rules heads) rules-and-heads
+    (if (zerop (set-size rules))
+      (list rules heads)
+      (labels ((negation-satisfied-p (negation)
+                 (not (set-lookup heads (bare-term negation))))
+               (rule-satisfied-p (rule)
+                 (every #'negation-satisfied-p (rule-body rule)))
+               (smallest-head ()
+                 (-<> (set->list rules)
+                   (mapcar #'rule-head <>)
+                   (sort <> #'term<)
+                   (first <>)))
+               (rules-with-head (head)
+                 (set-filter (lambda (rule) (eql head (rule-head rule)))
+                             rules)))
+        (let* ((next (smallest-head))
+               (candidates (rules-with-head next)))
+          (list (set-diff rules candidates)
+                (if (some #'rule-satisfied-p (set->list candidates))
+                  (set-insert heads next)
+                  heads)))))))
+
+
+(defun make-rule-tree (rules)
+  "Create a rule tree ZDD from the given logical `rules`.
+
+  `rules` should be a list of one layer-worth of rules, each of the form:
+  `(head-term &rest body-terms)`
+
+  Each head term should be a single variable.
+  Each body term should be either a single variable or `(not variable)`.
+
+  Rules and bodies do not need to be sorted beforehand.
+
+  "
+  (recursively ((rules (mapcar #'sort-body rules))
+                (accumulated-heads nil))
+    (let* ((heads (-<> rules
+                    (remove-if-not #'rule-empty-p <>)
+                    (mapcar #'rule-head <>)
+                    (remove-duplicates <> :test #'=)
+                    (union accumulated-heads <> :test #'=))) ; slow
+           (next-rules (remove-if
+                         (lambda (rule)
+                           (member (rule-head rule) heads :test #'equal))
+                         rules)))
+      (if (null next-rules)
+        (zdd-set heads)
+        (multiple-value-bind (term low high both)
+            (partition-rules next-rules)
+          ; (pr :rules rules)
+          ; (pr :acch accumulated-heads)
+          ; (pr :heads heads)
+          ; (pr :next-rules next-rules)
+          ; (pr :term term)
+          ; (pr :low low)
+          ; (pr :high high)
+          ; (pr :both both)
+          ; (break)
+          (zdd-node term
+                    (recur (append (mapcar #'drop-first high) both) heads)
+                    (recur (append (mapcar #'drop-first low) both) heads)))))))
+
diff -r 37e64253cccf -r addb56e3eb9d src/rule-trees.lisp
--- a/src/rule-trees.lisp	Sun Nov 20 15:33:06 2016 +0000
+++ b/src/rule-trees.lisp	Mon Nov 21 15:33:17 2016 +0000
@@ -68,50 +68,12 @@
                         (recur (append (mapcar #'rest disallows) ignores)))))))))
 
 
-;;;; GraphViz -----------------------------------------------------------------
-(setf cl-dot:*dot-path* "/usr/local/bin/dot")
-
-(defun attrs (object &rest attributes)
-  (make-instance 'cl-dot:attributed
-    :object object
-    :attributes attributes))
-
-
-(defmethod cl-dot:graph-object-node ((graph (eql 'rule-tree)) (object rule-tree))
-  (make-instance 'cl-dot:node
-    :attributes (adt:match rule-tree object
-                  ((node term _ _) `(:label ,(aesthetic-string term)
-                                     :shape :circle))
-
-                  (bottom `(:label "⊥"
-                            :shape :square))
-
-                  ((top term) `(:label ,(aesthetic-string term)
-                                :shape :rectangle)))))
-
-(defmethod cl-dot:graph-object-points-to ((graph (eql 'rule-tree))
-                                          (object rule-tree))
-  (adt:match rule-tree object
-    ((node _ hi lo) (list (attrs hi :style :solid)
-                          (attrs lo :style :dashed)))
-    ((top _) nil)
-    (bottom nil)))
-
-
-(defun draw (rule-tree &key (filename "rule-tree.png"))
-  (cl-dot:dot-graph
-    (cl-dot:generate-graph-from-roots 'rule-tree (list rule-tree))
-    filename
-    :format :png)
-  rule-tree)
-
-
 ;;;; Scratch ------------------------------------------------------------------
 (defparameter *rule* '(
-                       (1000 1 2 (ggp-rules::not 3))
-                       (1000 4 2 3 15)
-                       (1000 (ggp-rules::not 19) 18)
-                       (1000 19 17)
+                       (500 1 2 (ggp-rules::not 3))
+                       (500 4 2 3 15)
+                       (500 (ggp-rules::not 19) 18)
+                       (500 19 17)
                        ))
 
-(-<> *rule* make-rule-tree draw)
+(-<> *rule* make-rule-tree scully.graphviz::draw-rule-tree)
diff -r 37e64253cccf -r addb56e3eb9d src/terms.lisp
--- a/src/terms.lisp	Sun Nov 20 15:33:06 2016 +0000
+++ b/src/terms.lisp	Mon Nov 21 15:33:17 2016 +0000
@@ -245,19 +245,19 @@
 
 ;;;; Scratch ------------------------------------------------------------------
 
-(-<> '(
-       (ggp-rules::<= a (ggp-rules::true foo))
-       (ggp-rules::<= b (ggp-rules::true foo) (ggp-rules::true baz))
-       (ggp-rules::<= c (ggp-rules::true dogs) (ggp-rules::not a))
-       (ggp-rules::<= x (ggp-rules::not a) b)
-       (ggp-rules::<= y (ggp-rules::not a) (ggp-rules::not x))
-       (ggp-rules::<= y (ggp-rules::not c))
-       )
-  (integerize-rules <>)
-  (nth 2 <>)
-  (gethash :possible <>)
-  (stratify-layer <>)
-  (mapc (lambda (s) (format t "Stratum:~%~{    ~S~%~}" s)) <>)
-  (never <>)
-  ; (map nil #'print-hash-table <>)
-  )
+; (-<> '(
+;        (ggp-rules::<= a (ggp-rules::true foo))
+;        (ggp-rules::<= b (ggp-rules::true foo) (ggp-rules::true baz))
+;        (ggp-rules::<= c (ggp-rules::true dogs) (ggp-rules::not a))
+;        (ggp-rules::<= x (ggp-rules::not a) b)
+;        (ggp-rules::<= y (ggp-rules::not a) (ggp-rules::not x))
+;        (ggp-rules::<= y (ggp-rules::not c))
+;        )
+;   (integerize-rules <>)
+;   (nth 2 <>)
+;   (gethash :possible <>)
+;   (stratify-layer <>)
+;   (mapc (lambda (s) (format t "Stratum:~%~{    ~S~%~}" s)) <>)
+;   ; (never <>)
+;   ; (map nil #'print-hash-table <>)
+;   )
diff -r 37e64253cccf -r addb56e3eb9d src/zdd.lisp
--- a/src/zdd.lisp	Sun Nov 20 15:33:06 2016 +0000
+++ b/src/zdd.lisp	Mon Nov 21 15:33:17 2016 +0000
@@ -40,78 +40,6 @@
 (deftype sink () 'leaf)
 
 
-;;;; GraphViz -----------------------------------------------------------------
-(setf cl-dot:*dot-path* "/usr/local/bin/dot")
-(defparameter *draw-unique-sinks* nil)
-(defparameter *draw-unique-nodes* nil)
-(defparameter *draw-hex-p* #'never)
-(defparameter *draw-label-fn* #'identity)
-
-(defun attrs (object &rest attributes)
-  (make-instance 'cl-dot:attributed
-    :object object
-    :attributes attributes))
-
-
-(defun sink-attrs (val)
-  `(:label ,(if val "⊤" "⊥")
-    :shape :square
-    :style :filled
-    :fillcolor "#fafafa"
-    :color "#aaaaaa"
-    :fontsize 22
-    :width 0.05))
-
-(defmethod cl-dot:graph-object-node ((graph (eql 'zdd)) (object node))
-  (make-instance 'cl-dot:node
-    :attributes (ematch object
-                  ((node v) `(:label ,(funcall *draw-label-fn* v)
-                              :shape ,(if (funcall *draw-hex-p* v)
-                                        :hexagon
-                                        :rectangle))))))
-
-(defmethod cl-dot:graph-object-node ((graph (eql 'zdd)) (object cons))
-  (cl-dot:graph-object-node graph (car object)))
-
-(defmethod cl-dot:graph-object-node ((graph (eql 'zdd)) (object leaf))
-  (make-instance 'cl-dot:node
-    :attributes (ematch object ((sink c) (sink-attrs c)))))
-
-
-(defun wrap-node (object)
-  (ematch object
-    ((sink) (if *draw-unique-sinks* object (cons object nil)))
-    ((node) (if *draw-unique-nodes* object (cons object nil)))))
-
-(defmethod cl-dot:graph-object-points-to ((graph (eql 'zdd))
-                                          (object t))
-  (ematch object
-    ((cons object _)
-     (cl-dot:graph-object-points-to graph object))
-    ((sink _)
-     '())
-    ((node _ hi lo)
-     (list (attrs (wrap-node hi) :style :solid)
-           (attrs (wrap-node lo) :style :dashed)))))
-
-
-(defun draw (zdd &key
-             (filename "zdd.png")
-             (unique-sinks nil)
-             (unique-nodes t)
-             (hexp #'never)
-             (label-fn #'identity))
-  (let ((*draw-unique-sinks* unique-sinks)
-        (*draw-unique-nodes* unique-nodes)
-        (*draw-hex-p* hexp)
-        (*draw-label-fn* label-fn))
-    (cl-dot:dot-graph
-      (cl-dot:generate-graph-from-roots 'zdd (list (wrap-node zdd)))
-      filename
-      :format :png))
-  zdd)
-
-
 ;;;; ZDDs ---------------------------------------------------------------------
 (defparameter *cache*
   (tg:make-weak-hash-table :weakness :value :test #'equalp))
@@ -410,156 +338,6 @@
   (zdd-match% zdd (sort set #'<) lower-bound upper-bound))
 
 
-;;;; Rule Trees ---------------------------------------------------------------
-(defun rule-head (rule)
-  (first rule))
-
-(defun rule-body (rule)
-  (rest rule))
-
-(defun rule-first-body (rule)
-  (first (rule-body rule)))
-
-(defun rule-empty-p (rule)
-  (null (rule-body rule)))
-
-
-(defun negationp (term)
-  (and (consp term) (eql 'ggp-rules::not (first term))))
-
-(defun bare-term (term)
-  (if (negationp term)
-    (second term)
-    term))
-
-(defun term< (t1 t2)
-  (< (bare-term t1) (bare-term t2)))
-
-
-(defun sort-body (rule)
-  (destructuring-bind (head . body) rule
-    (list* head (sort body #'term<))))
-
-(defun drop-first (rule)
-  (destructuring-bind (head . body) rule
-    (list* head (rest body))))
-
-(defun find-smallest-body-term (rules)
-  (-<> rules
-    (mapcar #'rule-first-body <>)
-    (sort <> #'term<)
-    (first <>)))
-
-(defun partition-rules (rules)
-  (let ((element (bare-term (find-smallest-body-term rules))))
-    (labels
-        ((rule-requires (rule)
-           (equal (rule-first-body rule) element))
-         (rule-disallows (rule)
-           (equal (rule-first-body rule) `(ggp-rules::not ,element)))
-         (rule-ignores (rule)
-           (not (or (rule-requires rule)
-                    (rule-disallows rule)))))
-      (values element
-              (remove-if-not #'rule-disallows rules)
-              (remove-if-not #'rule-requires rules)
-              (remove-if-not #'rule-ignores rules)))))
-
-
-(defmethod print-object ((set hash-set) stream)
-  (print-unreadable-object (set stream :type t :identity nil)
-    (prin1 (set->list set) stream)))
-
-(defun hash-set= (s1 s2)
-  (zerop (set-size (set-symmetric-diff s1 s2))))
-
-(defun rule-head-in (set rule)
-  (set-lookup set (rule-head rule)))
-
-(defun collapse-positive-heads (rules-and-heads)
-  (destructuring-bind (rules heads) rules-and-heads
-    (flet ((update-rule (rule)
-             (cons (rule-head rule)
-                   (remove-if (curry #'set-lookup heads)
-                              (rule-body rule)))))
-      (let* ((new-rules (set-map #'update-rule rules))
-             (new-heads (-<> new-rules
-                          (set-filter #'rule-empty-p <>)
-                          (set-map #'rule-head <>))))
-        (list (set-filter (complement (curry #'rule-head-in new-heads))
-                          new-rules)
-              (set-union heads new-heads))))))
-
-(defun find-strictly-negative-rules (rules)
-  (set-filter (lambda (rule)
-                (every #'negationp (rule-body rule)))
-              rules))
-
-(defun collapse-negative-heads (rules-and-heads)
-  (destructuring-bind (rules heads) rules-and-heads
-    (if (zerop (set-size rules))
-      (list rules heads)
-      (labels ((negation-satisfied-p (negation)
-                 (not (set-lookup heads (bare-term negation))))
-               (rule-satisfied-p (rule)
-                 (every #'negation-satisfied-p (rule-body rule)))
-               (smallest-head ()
-                 (-<> (set->list rules)
-                   (mapcar #'rule-head <>)
-                   (sort <> #'term<)
-                   (first <>)))
-               (rules-with-head (head)
-                 (set-filter (lambda (rule) (eql head (rule-head rule)))
-                             rules)))
-        (let* ((next (smallest-head))
-               (candidates (rules-with-head next)))
-          (list (set-diff rules candidates)
-                (if (some #'rule-satisfied-p (set->list candidates))
-                  (set-insert heads next)
-                  heads)))))))
-
-
-(defun make-rule-tree (rules)
-  "Create a rule tree ZDD from the given logical `rules`.
-
-  `rules` should be a list of one layer-worth of rules, each of the form:
-  `(head-term &rest body-terms)`
-
-  Each head term should be a single variable.
-  Each body term should be either a single variable or `(not variable)`.
-
-  Rules and bodies do not need to be sorted beforehand.
-
-  "
-  (recursively ((rules (mapcar #'sort-body rules))
-                (accumulated-heads nil))
-    (let* ((heads (-<> rules
-                    (remove-if-not #'rule-empty-p <>)
-                    (mapcar #'rule-head <>)
-                    (remove-duplicates <> :test #'=)
-                    (union accumulated-heads <> :test #'=))) ; slow
-           (next-rules (remove-if
-                         (lambda (rule)
-                           (member (rule-head rule) heads :test #'equal))
-                         rules)))
-      (if (null next-rules)
-        (zdd-set heads)
-        (multiple-value-bind (term low high both)
-            (partition-rules next-rules)
-          ; (pr :rules rules)
-          ; (pr :acch accumulated-heads)
-          ; (pr :heads heads)
-          ; (pr :next-rules next-rules)
-          ; (pr :term term)
-          ; (pr :low low)
-          ; (pr :high high)
-          ; (pr :both both)
-          ; (break)
-          (zdd-node term
-                    (recur (append (mapcar #'drop-first high) both) heads)
-                    (recur (append (mapcar #'drop-first low) both) heads)))))))
-
-
 (defun apply-rule-tree (zdd rule-tree head-bound)
   "Apply the logical rules in `rule-tree` to the sets in `zdd`.