# HG changeset patch # User Steve Losh # Date 1485088665 0 # Node ID e36b35a1857f702788fa09c44db1a992ecfeeeb2 # Parent b8e4476045c24dd7aa4cae047e25184eea85cb5d Add `(next ...)` -> `(true ...)` conversion diff -r b8e4476045c2 -r e36b35a1857f src/reasoners/zdd.lisp --- 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* <>) ))) diff -r b8e4476045c2 -r e36b35a1857f src/terms.lisp --- 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 <>) + )