# HG changeset patch # User Steve Losh # Date 1481824998 18000 # Node ID 41b2461432fcbc20346291eda1de3f78bd57d99e # Parent 51bc78b22d98541ca2b196d13506c3bc357cca46 Implement the basic iset traversal logic diff -r 51bc78b22d98 -r 41b2461432fc package.lisp --- a/package.lisp Sun Dec 11 16:32:58 2016 -0500 +++ b/package.lisp Thu Dec 15 13:03:18 2016 -0500 @@ -44,7 +44,27 @@ :trivia :trivialib.bdd :scully.quickutils) - (:export) + (:export + :node + :sink + :content + :with-zdd + :zdd-node + :zdd-empty-p + :zdd-unit-p + :zdd-count + :zdd-size + :zdd-random-member + :zdd-set + :zdd-union + :zdd-intersection + :zdd-join + :zdd-meet + :zdd-family + :zdd-keep-supersets-of + :zdd-remove-supersets-of + :zdd-keep-avoiders-of + :zdd-match) (:shadowing-import-from :hamt :hash-set)) @@ -102,6 +122,7 @@ :iterate :trivia :cl-arrows + :scully.zdd :scully.quickutils)) diff -r 51bc78b22d98 -r 41b2461432fc src/reasoners/zdd.lisp --- a/src/reasoners/zdd.lisp Sun Dec 11 16:32:58 2016 -0500 +++ b/src/reasoners/zdd.lisp Thu Dec 15 13:03:18 2016 -0500 @@ -1,22 +1,19 @@ (in-package :scully.reasoners.zdd) -(defparameter *rules* - (scully.gdl::read-gdl "gdl/tictactoe-grounded.gdl") - ; (scully.gdl::read-gdl "gdl/hanoi-grounded.gdl") - ; (scully.gdl::read-gdl "gdl/8puzzle-grounded.gdl") - ; (scully.gdl::read-gdl "gdl/roshambo2-grounded.gdl") - ) - - +;;;; Utils -------------------------------------------------------------------- (defmacro defclass* (name-and-options direct-superclasses slots &rest options) (flet ((slot-definition (conc-name slot) (destructuring-bind (name &key type documentation + initform (accessor (symb conc-name name)) (initarg (intern (symbol-name name) :keyword))) (ensure-list slot) - `(,name :initarg ,initarg :accessor ,accessor + `(,name + :initarg ,initarg + :accessor ,accessor + ,@(when initform `(:initform ,initform)) ,@(when type `(:type ,type)) ,@(when documentation `(:documentation ,documentation)))))) (destructuring-bind (name &key (conc-name (symb name '-))) @@ -25,6 +22,35 @@ ,(mapcar (curry #'slot-definition conc-name) slots) ,@options)))) + +;;;; Rule Forests ------------------------------------------------------------- +(defclass* (rule-forest :conc-name rf-) () + (strata + upper-bound + lower-bound)) + + +(defun make-forest-with (old-forest strata) + (make-instance 'rule-forest + :strata strata + :upper-bound (rf-upper-bound old-forest) + :lower-bound (rf-lower-bound old-forest))) + +(defun forest-empty-p (forest) + (null (rf-strata forest))) + + +(defun find-bound (predicate layer) + (extremum (mapcar #'scully.gdl::rule-head layer) predicate)) + +(defun find-lower-bound (layer) + (find-bound #'< layer)) + +(defun find-upper-bound (layer) + (find-bound #'> layer)) + + +;;;; Reasoner ----------------------------------------------------------------- (defclass* (zdd-reasoner :conc-name zr-) () (rules roles @@ -59,7 +85,7 @@ (eql predicate (first (first rule)))) <>) (mapcar #'cdr <>) - (scully.zdd::zdd-set <>))) + (zdd-set <>))) (defun make-stratum-rule-trees (stratum) (-<> stratum @@ -67,6 +93,15 @@ hash-table-values (mapcar #'scully.rule-trees::make-rule-tree <>))) +(defun make-rule-forest (rule-layers layer) + (let ((rules (gethash layer rule-layers))) + (make-instance 'rule-forest + :strata (-<> rules + scully.terms::stratify-layer + (mapcar #'make-stratum-rule-trees <>)) + :upper-bound (find-upper-bound rules) + :lower-bound (find-lower-bound rules)))) + (defun make-zdd-reasoner (rules) "Turn a set of grounded GDL rules into a logic manager. @@ -86,106 +121,208 @@ (let ((rules (scully.gdl::normalize-rules rules))) (destructuring-bind (term->number number->term rule-layers) (scully.terms::integerize-rules rules) - (flet ((make-forest (layer) - (-<> rule-layers - (gethash layer <>) - scully.terms::stratify-layer - (mapcar #'make-stratum-rule-trees <>)))) - (scully.zdd::with-zdd - (make-instance 'zdd-reasoner - :rules rules - :roles (find-roles rules) - :possible-forest (make-forest :possible) - :happens-forest (make-forest :happens) - :initial-zdd (scully.zdd::zdd-set (find-initial-state rules term->number)) - :legal-zdd (make-predicate-zdd 'ggp-rules::legal term->number) - :goal-zdd (make-predicate-zdd 'ggp-rules::goal term->number) - :terminal-zdd (make-predicate-zdd 'ggp-rules::terminal term->number) - :term->number term->number - :number->term number->term)))))) + (with-zdd + (make-instance 'zdd-reasoner + :rules rules + :roles (find-roles rules) + :possible-forest (make-rule-forest rule-layers :possible) + :happens-forest (make-rule-forest rule-layers :happens) + :initial-zdd (zdd-set (find-initial-state rules term->number)) + :legal-zdd (make-predicate-zdd 'ggp-rules::legal term->number) + :goal-zdd (make-predicate-zdd 'ggp-rules::goal term->number) + :terminal-zdd (make-predicate-zdd 'ggp-rules::terminal term->number) + :term->number term->number + :number->term number->term))))) -(defun initial-iset (reasoner) - "Return the initial information set of the game." - (zr-initial-zdd reasoner)) - +;;;; Basic API ---------------------------------------------------------------- (defun number-to-term (reasoner number) (gethash number (zr-number->term reasoner))) (defun term-to-number (reasoner term) (gethash term (zr-term->number reasoner))) + +(defun initial-iset (reasoner) + "Return the initial information set of the game." + (zr-initial-zdd reasoner)) + (defun rand-state (reasoner iset) "Select a random member of the given information set." (mapcar (curry #'number-to-term reasoner) - (scully.zdd::zdd-random-member iset))) + (zdd-random-member iset))) (defun terminalp (reasoner iset) "Return whether the given information set is a terminal state." (-<> iset - (scully.zdd::zdd-meet <> (zr-terminal-zdd reasoner)) - scully.zdd::zdd-unit-p + (zdd-meet <> (zr-terminal-zdd reasoner)) + zdd-unit-p not)) +(defun roles (reasoner) + (zr-roles reasoner)) + + +;;;; Drawing ------------------------------------------------------------------ +(defun label (reasoner n) + (let ((*package* (find-package :ggp-rules))) + (-<> n + (number-to-term reasoner <>) + (structural-string <>)))) + (defun draw-zdd (reasoner zdd) - (flet ((label (n) - (let ((*package* (find-package :ggp-rules))) - (-<> n - (number-to-term reasoner <>) - (structural-string <>))))) - (scully.graphviz::draw-zdd zdd :label-fn #'label))) + (scully.graphviz::draw-zdd zdd :label-fn (curry #'label reasoner))) + +(defun draw-rule-tree (reasoner rule-tree) + (scully.graphviz::draw-rule-tree rule-tree :label-fn (curry #'label reasoner))) + + +;;;; Logic Application -------------------------------------------------------- +(defun tree-to-result (tree) + (adt:match scully.rule-trees::rule-tree tree + ((scully.rule-trees::top head) (values nil head)) + (scully.rule-trees::bottom (values nil nil)) + ((scully.rule-trees::node _ _ _) (values tree nil)))) -(defparameter *l* (make-zdd-reasoner *rules*)) +(defun process-stratum (function stratum) + "Process the stratum with `function`. + + Two values will be returned: + + 1. The new stratum (possibly NIL). + 2. Any new heads to add (possible NIL). + + " + (iterate + (for tree :in stratum) + (for (values new-tree new-head) = (funcall function tree)) + (when new-tree (collect new-tree :into new-stratum)) + (when new-head (collect new-head :into new-heads)) + (finally (return (values new-stratum new-heads))))) + +(defun process-forest (function forest) + "Process the rule forest with `function`. + + Two values will be returned: + + 1. The new forest (possibly NIL). + 2. Any new heads to add (possible NIL). + + " + (iterate + (for stratum :in (rf-strata forest)) + (for (values new-stratum new-heads) = (process-stratum function stratum)) + (when new-stratum (collect new-stratum :into new-strata)) + (appending new-heads :into heads) + (finally (return (values (make-forest-with forest new-strata) heads))))) -; (defun apply-rule-tree (zdd rule-tree head-bound) -; "Apply the logical rules in `rule-tree` to the sets in `zdd`. +(defun advance-tree (tree term) + "Advance the rule tree up to (but not beyond) `term`. -; `zdd` is assumed to contain sets of logical axioms. This function will update -; each of these sets to add any rule heads derivable from the axioms in the set. + Two values will be returned: + + 1. Either the resulting rule tree, or NIL if it was advanced down to a sink. + 2. The new head if it was advanced down to a TOP sink, or NIL otherwise. -; " -; (recursively ((zdd zdd) -; (rule-tree rule-tree)) -; (ematch* (zdd rule-tree) -; ;; If Z = ∅ there are no sets to cons heads onto, bail. -; (((sink nil) _) zdd) + " + (adt:match scully.rule-trees::rule-tree tree + ((scully.rule-trees::node term% _ lo) + (if (< term% term) + (advance-tree lo term) + (tree-to-result tree))) + (_ (tree-to-result tree)))) -; ;; If R = ∅ or {∅} we've bottomed out of the rule tree and there are no -; ;; heads to cons, we're done. -; ((_ (sink)) zdd) +(defun advance-forest (forest term) + "Advance the rule forest up to (but not beyond) `term`. + + Two values will be returned: + + 1. The new forest (possibly NIL). + 2. Any new heads to add (possible NIL). -; ;; 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)) + " + (process-forest (rcurry #'advance-tree term) forest)) + -; ;; If Z = {∅} we might have some heads we need to cons later in the rule -; ;; tree, so recur down the lo side of it. -; (((sink t) (node _ _ lo)) -; (recur zdd lo)) +(defun split-tree-hi (tree term) + (adt:match scully.rule-trees::rule-tree tree + ((scully.rule-trees::node term% hi _) + (if (= term% term) + (tree-to-result hi) + (tree-to-result tree))) + (_ (error "Cannot split rule tree: ~S" tree)))) -; ;; 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))))))) +(defun split-tree-lo (tree term) + (adt:match scully.rule-trees::rule-tree tree + ((scully.rule-trees::node term% _ lo) + (if (= term% term) + (tree-to-result lo) + (tree-to-result tree))) + (_ (error "Cannot split rule tree: ~S" tree)))) + + +(defun split-forest-hi (forest term) + (process-forest (rcurry #'split-tree-hi term) forest)) + +(defun split-forest-lo (forest term) + (process-forest (rcurry #'split-tree-lo term) forest)) +(defun finalize-heads (reasoner forest heads) + "Finalize the set of heads to add and return the appropriate ZDD." + (prl reasoner forest heads) + (zdd-set heads)) -;;;; PLAN -;;; -;;; 1. Receive GDL from server -;;; 2. Ground it -;;; 3. Integerize the ground GDL -;;; 4. Find initial state -;;; 5. Build rule trees for integerized rules -;;; 6. ... +(defun traverse-iset (reasoner iset forest) + "Walk down the information set and rule forest in parallel." + (declare (ignorable reasoner)) + (recursively ((iset iset) + (forest forest) + (heads '())) + (ematch iset + ;; If we hit an empty sink we're out of sets to ever cons the heads onto, + ;; so we can just bail immediately. + ((sink nil) iset) + + ;; If we hit a unit sink we're done with the state-walking portion of this + ;; algorithm and can move on the the fixed-pointing of the heads. + ((sink t) (finalize-heads reasoner forest heads)) + + ;; Otherwise we need to build a new ZDD node with the recursive results. + ((node term hi lo) + (multiple-value-bind* + (((forest advanced-heads) (advance-forest forest term)) + ((forest-hi hi-heads) (split-forest-hi forest term)) + ((forest-lo lo-heads) (split-forest-lo forest term))) + (zdd-node + term + (recur hi forest-hi (append heads advanced-heads hi-heads)) + (recur lo forest-lo (append heads advanced-heads lo-heads)))))))) + + +(defun apply-rule-forest (reasoner iset forest) + "Apply `forest` to the given information set for `reasoner`." + (declare (ignorable reasoner)) + (with-zdd + (traverse-iset reasoner iset forest))) + + +;;;; Scratch ------------------------------------------------------------------ +(defparameter *rules* + (scully.gdl::read-gdl "gdl/tictactoe-grounded.gdl") + ; (scully.gdl::read-gdl "gdl/hanoi-grounded.gdl") + ; (scully.gdl::read-gdl "gdl/8puzzle-grounded.gdl") + ; (scully.gdl::read-gdl "gdl/roshambo2-grounded.gdl") + ) +(defparameter *l* (make-zdd-reasoner *rules*)) + +; (draw-zdd *l* (initial-iset *l*)) + +; (-<> *l* +; (apply-rule-forest <> (initial-iset *l*) (zr-possible-forest *l*)) +; (draw-zdd *l* <>) +; (no <>) +; ) diff -r 51bc78b22d98 -r 41b2461432fc src/rule-trees.lisp --- a/src/rule-trees.lisp Sun Dec 11 16:32:58 2016 -0500 +++ b/src/rule-trees.lisp Thu Dec 15 13:03:18 2016 -0500 @@ -7,6 +7,16 @@ (top t) bottom) +(defun rule-tree-hi (tree) + (adt:match rule-tree tree + ((node _ hi _) hi) + (_ (error "No hi for rule tree ~S" tree)))) + +(defun rule-tree-lo (tree) + (adt:match rule-tree tree + ((node _ _ lo) lo) + (_ (error "No lo for rule tree ~S" tree)))) + (defun find-smallest-body-term (bodies) "Find the smallest body term in `bodies`. @@ -84,4 +94,11 @@ (500 19 17) )) -; (-<> *rule* make-rule-tree scully.graphviz::draw-rule-tree) +; (-<> *rule* +; make-rule-tree +; (rule-tree-hi <>) +; (rule-tree-hi <>) +; ; (advance-tree <> 6) +; scully.graphviz::draw-rule-tree +; ; scully.graphviz::draw-rule-tree +; ) diff -r 51bc78b22d98 -r 41b2461432fc vendor/quickutils.lisp --- a/vendor/quickutils.lisp Sun Dec 11 16:32:58 2016 -0500 +++ b/vendor/quickutils.lisp Thu Dec 15 13:03:18 2016 -0500 @@ -2,7 +2,7 @@ ;;;; See http://quickutil.org for details. ;;;; To regenerate: -;;;; (qtlc:save-utils-as "quickutils.lisp" :utilities '(:COMPOSE :COPY-HASH-TABLE :CURRY :ENSURE-BOOLEAN :ENSURE-GETHASH :ENSURE-LIST :EXTREMUM :FLATTEN-ONCE :HASH-TABLE-ALIST :HASH-TABLE-KEYS :HASH-TABLE-VALUES :MAP-PRODUCT :MKSTR :ONCE-ONLY :RCURRY :SET-EQUAL :SUBDIVIDE :SYMB :WITH-GENSYMS :WITH-OUTPUT-TO-FILE :WRITE-STRING-INTO-FILE :YES-NO) :ensure-package T :package "SCULLY.QUICKUTILS") +;;;; (qtlc:save-utils-as "quickutils.lisp" :utilities '(:COMPOSE :EXTREMUM :COPY-HASH-TABLE :CURRY :ENSURE-BOOLEAN :ENSURE-GETHASH :ENSURE-LIST :EXTREMUM :FLATTEN-ONCE :HASH-TABLE-ALIST :HASH-TABLE-KEYS :HASH-TABLE-VALUES :MAP-PRODUCT :MKSTR :ONCE-ONLY :RCURRY :SET-EQUAL :SUBDIVIDE :SYMB :WITH-GENSYMS :WITH-OUTPUT-TO-FILE :WRITE-STRING-INTO-FILE :YES-NO) :ensure-package T :package "SCULLY.QUICKUTILS") (eval-when (:compile-toplevel :load-toplevel :execute) (unless (find-package "SCULLY.QUICKUTILS")