Add `(next ...)` -> `(true ...)` conversion
author |
Steve Losh <steve@stevelosh.com> |
date |
Sun, 22 Jan 2017 12:37:45 +0000 |
parents |
b8e4476045c2
|
children |
9cdd37548c6f
|
branches/tags |
(none) |
files |
src/reasoners/zdd.lisp src/terms.lisp |
Changes
--- a/src/reasoners/zdd.lisp Sat Jan 21 12:52:12 2017 +0000
+++ b/src/reasoners/zdd.lisp Sun Jan 22 12:37:45 2017 +0000
@@ -149,6 +149,20 @@
:number->term number->term)))))
+;;;; State Conversion ---------------------------------------------------------
+(defun convert-next-to-true (reasoner zdd)
+ (recursively ((z zdd))
+ (ematch z
+ ((sink nil) (sink nil))
+ ((sink t) (sink t))
+ ((node n hi lo)
+ (ematch (number-to-term reasoner n)
+ (`(ggp-rules::next ,body)
+ (zdd-node (term-to-number reasoner `(ggp-rules::true ,body))
+ (recur hi)
+ (recur lo))))))))
+
+
;;;; Basic API ----------------------------------------------------------------
(defun number-to-term (reasoner number)
(gethash number (zr-number->term reasoner)))
@@ -468,6 +482,8 @@
(apply-rule-forest *r* <> (zr-happens-forest *r*))
(zdd-meet <> (zr-next-zdd *r*))
(dump-iset *r* <>)
+ (convert-next-to-true *r* <>)
+ (dump-iset *r* <>)
(no <>)
; (draw-zdd *r* <>)
)))
--- a/src/terms.lisp Sat Jan 21 12:52:12 2017 +0000
+++ b/src/terms.lisp Sun Jan 22 12:37:45 2017 +0000
@@ -232,6 +232,20 @@
(append leftovers strata-terms)))
+(defun sort-base-layer (base-terms happens-terms)
+ "Return a fresh list of the base terms, sorted correctly."
+ ;; The base layer needs to be sorted in the same order as the `next` terms
+ ;; appear in the `happens` layer, because we want to be able to convert a ZDD
+ ;; of `(next ...)` terms into the next information set in a single pass.
+ (sort (copy-seq base-terms) #'<
+ :key (trivia:lambda-match
+ (`(ggp-rules::true ,body)
+ (or (position `(ggp-rules::next ,body) happens-terms
+ :test #'equal)
+ -1))
+ (_ -2))))
+
+
(defun order-terms (rules)
"Find a linear ordering of all terms in `rules`.
@@ -251,10 +265,10 @@
(possible-strata (stratify-layer possible-rules))
(happens-strata (stratify-layer happens-rules)))
;; We order the individual layers.
- (let ((base-terms (gethash :base layers))
- (does-terms (gethash :does layers))
- (possible-terms (order-layer (gethash :possible layers) possible-strata))
- (happens-terms (order-layer (gethash :happens layers) happens-strata)))
+ (let* ((possible-terms (order-layer (gethash :possible layers) possible-strata))
+ (happens-terms (order-layer (gethash :happens layers) happens-strata))
+ (base-terms (sort-base-layer (gethash :base layers) happens-terms))
+ (does-terms (gethash :does layers)))
;; And finally we concatenate the layer orderings into one bigass order:
;; base < possible < does < happens
(values (append base-terms possible-terms does-terms happens-terms)
@@ -310,12 +324,11 @@
'(
(ggp-rules::<= x (ggp-rules::true a))
(ggp-rules::<= x (ggp-rules::true b))
- (ggp-rules::<= y (ggp-rules::true b) (ggp-rules::not z))
- (ggp-rules::<= z (ggp-rules::not x) foo)
- (ggp-rules::<= dogs (ggp-rules::not y))
- (ggp-rules::<= dogs (ggp-rules::true cats))
- (ggp-rules::<= mice (ggp-rules::does player something))
- ; (ggp-rules::<= cats (ggp-rules::does player something) x)
+ (ggp-rules::<= (ggp-rules::next a)
+ (ggp-rules::true dangus))
+ (ggp-rules::<= z (ggp-rules::does c x))
+ (ggp-rules::<= (ggp-rules::next b)
+ (ggp-rules::not z))
))
(defun print-strata (strata)
@@ -324,12 +337,12 @@
(format t "STRATUM ~D:~%~{ ~S~%~}~2%"
i stratum)))
-; (-<> *rules*
-; (normalize-rules <>)
-; (integerize-rules <>)
-; ; (nth 2 <>)
-; ; (print-strata <>)
-; (no <>)
-; ; (rest <>)
-; ; (map nil #'print-hash-table <>)
-; )
+(-<> *rules*
+ (normalize-rules <>)
+ (integerize-rules <>)
+ ; (nth 2 <>)
+ ; (print-strata <>)
+ (no <>)
+ ; (rest <>)
+ ; (map nil #'print-hash-table <>)
+ )