--- 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))
--- 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 <>)
+; )
--- 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
+; )
--- 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")