--- 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
--- 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
--- /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)
+
--- /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)))))))
+
--- 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)
--- 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 <>)
+; )
--- 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`.