# HG changeset patch
# User Steve Losh <steve@stevelosh.com>
# Date 1478013635 0
# Node ID 8e281422161dc7cf2934e857e323b095c59c34e6
# Parent  089d9e0ffbc76d6a5864da6ec7326681309f3aa6
Port old rule tree implementation to ZDDs & implement basic rule tree reasoning

diff -r 089d9e0ffbc7 -r 8e281422161d scully.asd
--- a/scully.asd	Tue Nov 01 14:20:24 2016 +0000
+++ b/scully.asd	Tue Nov 01 15:20:35 2016 +0000
@@ -26,7 +26,6 @@
                (:file "package")
                (:module "src" :serial t
                 :components ((:file "gdl")
-                             (:file "rule-trees")
                              (:file "zdd")
                              (:module "reasoners" :serial t
                               :components ((:file "prolog")))
diff -r 089d9e0ffbc7 -r 8e281422161d src/rule-trees.lisp
--- a/src/rule-trees.lisp	Tue Nov 01 14:20:24 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,156 +0,0 @@
-(in-package :scully.rule-trees)
-
-
-(adt:defdata rule-tree
-  (node t rule-tree rule-tree)
-  (leaf list))
-
-
-(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 'not (first term))))
-
-(defun bare-term (term)
-  (if (negationp term)
-    (second term)
-    term))
-
-
-(defun %term< (t1 t2)
-  ;; symbol < number < cons
-  (ensure-boolean
-    (etypecase t1
-      (symbol (etypecase t2
-                (symbol (string< (symbol-name t1) (symbol-name t2)))
-                (number t)
-                (cons t)))
-      (number (etypecase t2
-                (symbol nil)
-                (number (< t1 t2))
-                (cons t)))
-      (cons (etypecase t2
-              (symbol nil)
-              (number nil)
-              (cons (cond
-                      ((term< (car t1) (car t2)) t)
-                      ((term< (car t2) (car t1)) nil)
-                      (t (term< (cdr t1) (cdr t2))))))))))
-(defun term< (t1 t2)
-  ;; symbol < number < cons
-  (%term< (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) `(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)))))
-
-
-(defun make-rule-tree (rules)
-  (recursively ((rules (mapcar #'sort-body rules))
-                (accumulated-heads nil))
-    (let* ((heads (-<> rules
-                    (remove-if-not #'rule-empty-p <>)
-                    (mapcar #'rule-head <>)
-                    (remove-duplicates <> :test #'equal)
-                    (union accumulated-heads <> :test #'equal))) ; slow
-           (next-rules (remove-if
-                         (lambda (rule)
-                           (member (rule-head rule) heads :test #'equal))
-                         rules)))
-      (if (null next-rules)
-        (leaf heads)
-        (multiple-value-bind (term low high both)
-            (partition-rules next-rules)
-          (node term
-                (recur (append (mapcar #'drop-first low) both) heads)
-                (recur (append (mapcar #'drop-first high) both) heads)))))))
-
-
-;;;; GraphViz
-(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 'rule-tree))
-                                     (object rule-tree))
-  (make-instance 'cl-dot:node
-                 :attributes (adt:match rule-tree object
-                               ((leaf heads)
-                                `(:label ,(structural-string heads)
-                                  :shape :ellipse))
-                               ((node term _ _)
-                                `(:label ,(structural-string term)
-                                  :shape :box)))))
-
-(defmethod cl-dot:graph-object-points-to ((graph (eql 'rule-tree))
-                                          (object rule-tree))
-  (adt:match rule-tree object
-    ((leaf _) nil)
-    ((node _ low high)
-     (list (attrs high :style :solid)
-           (attrs low :style :dashed)))))
-
-(defun draw-rule-tree (tree &optional (filename "tree.png"))
-  (cl-dot:dot-graph
-    (cl-dot:generate-graph-from-roots 'rule-tree (list tree))
-    filename
-    :format :png))
-
-
-;;;; Scratch
-(defparameter *rules* '(
-                        (x (not b) a)
-                        (x a c)
-                        (y c)
-                        (z b d)
-                        (z d (not c))
-                        ))
-(defparameter *rules* '(
-                        (x (not b) a)
-                        (x a c)
-                        (y c)
-                        (z d b)
-                        (z (not c) d)
-                        ))
-
-(draw-rule-tree (make-rule-tree *rules*))
diff -r 089d9e0ffbc7 -r 8e281422161d src/zdd.lisp
--- a/src/zdd.lisp	Tue Nov 01 14:20:24 2016 +0000
+++ b/src/zdd.lisp	Tue Nov 01 15:20:35 2016 +0000
@@ -12,6 +12,18 @@
 (defpattern leaf (&optional content)
   `(structure leaf :content ,content))
 
+(defun never (val)
+  (declare (ignore val))
+  (values))
+
+(defun print-through (function val)
+  (pr (funcall function val))
+  val)
+
+(defun mapprint-through (function val)
+  (mapc #'pr (funcall function val))
+  val)
+
 
 ;;;; GraphViz -----------------------------------------------------------------
 (setf cl-dot:*dot-path* "/usr/local/bin/dot")
@@ -90,10 +102,6 @@
      (append (mapcar (curry #'cons variable) (enumerate hi))
              (enumerate lo)))))
 
-(defun print-enumerated (zdd)
-  (pr (enumerate zdd))
-  zdd)
-
 
 (defun zdd-count (zdd)
   "Return the number of members of `zdd`."
@@ -283,6 +291,117 @@
   (reduce #'zdd-union (mapcar #'zdd-set sets)))
 
 
+;;;; 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 '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) `(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)))))
+
+
+(defun make-rule-tree (rules)
+  (recursively ((rules (mapcar #'sort-body rules))
+                (accumulated-heads nil))
+    (let* ((heads (-<> rules
+                    (remove-if-not #'rule-empty-p <>)
+                    (mapcar #'rule-head <>)
+                    (remove-duplicates <> :test #'equal)
+                    (union accumulated-heads <> :test #'equal))) ; 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)
+            (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)
+  (recursively ((zdd zdd)
+                (rule-tree rule-tree))
+    (ematch* (zdd rule-tree)
+      ;; If Z = ∅ there are no sets to cons heads onto, bail.
+      (((leaf nil) _) zdd)
+
+      ;; If R = ∅ or {∅} we've bottomed out of the rule tree and there are no
+      ;; heads to cons, we're done.
+      ((_ (leaf)) zdd)
+
+      ;; If we've passed the head boundary on the rule tree side then we're done
+      ;; filtering and just need to cons in all the heads.
+      ((_ (guard (node var _ _)
+                 (>= var head-bound)))
+       (zdd-join zdd rule-tree))
+
+      ;; If Z = {∅} we might have some heads we need to cons later in the rule
+      ;; tree, so recur down the lo side of it.
+      (((leaf t) (node _ _ lo))
+       (recur zdd lo))
+
+      ;; Otherwise we need to filter.
+      (((node var-z hi-z lo-z) (node var-r hi-r lo-r))
+       (cond
+         ((= var-z var-r) (zdd-node var-z
+                                    (recur hi-z hi-r)
+                                    (recur lo-z lo-r)))
+         ((< var-z var-r) (zdd-node var-z
+                                    (recur hi-z rule-tree)
+                                    (recur lo-z rule-tree)))
+         ((> var-z var-r) (recur zdd lo-r)))))))
+
+
 ;;;; Scratch ------------------------------------------------------------------
 (let ((*draw-unique-sinks* nil))
   (with-zdd
@@ -295,3 +414,58 @@
       (draw <>)
       (zdd-size <>)
       )))
+
+(defparameter *rules* '(
+                        (1001 (not 2) 1)
+                        (1001 1 3)
+                        (1002 3)
+                        (1003 4 2)
+                        (1003 (not 3) 4)
+                        (1004 1 2 3 (not 4))
+                        (1005 (not 2) (not 3))
+                        (1006 4 5)
+                        (1006 2)
+                        ))
+
+(defparameter *state* '(
+                        (1 3)
+                        (1 2)
+                        (2 4 5)
+                        ()
+                        (1 2 4 7)
+                        )
+  )
+
+(let ((*draw-unique-sinks* t))
+  (with-zdd
+    (-<> (make-rule-tree *rules*)
+      ; (print-enumerated <>)
+      ; (zdd-keep-avoiders-of <> '(2 7))
+      (mapprint-through #'enumerate <>)
+      (print-through #'zdd-count <>)
+      (print-through #'zdd-size <>)
+      (draw <>)
+      ; (zdd-size <>)
+      (never)
+      )
+    (pr '--------------)
+    (-<> (apply #'zdd-family *state*)
+      (mapprint-through #'enumerate <>)
+      (print-through #'zdd-count <>)
+      (print-through #'zdd-size <>)
+      ; (draw <>)
+      ; (zdd-size <>)
+      (never)
+      )
+    (pr '--------------)
+    (-<> (apply-rule-tree (apply #'zdd-family *state*)
+                          (make-rule-tree *rules*)
+                          100)
+      (mapprint-through #'enumerate <>)
+      (print-through #'zdd-count <>)
+      (print-through #'zdd-size <>)
+      ; (draw <>)
+      ; (zdd-size <>)
+      (never)
+      )
+    ))