# HG changeset patch # User Steve Losh # Date 1478348556 0 # Node ID 7fe3a52bf1f643fdf1b49ccd7b1fbc9166616551 # Parent d505235f4520b3b97df4f479e35733e8153e06cb Initial stab and the head collapsing. Not 100% sure I've got this right... diff -r d505235f4520 -r 7fe3a52bf1f6 package.lisp --- a/package.lisp Wed Nov 02 13:21:21 2016 +0000 +++ b/package.lisp Sat Nov 05 12:22:36 2016 +0000 @@ -11,14 +11,6 @@ :load-rules :redump-gdl)) -(defpackage :scully.rule-trees - (:use - :cl - :losh - :iterate - :cl-arrows - :scully.quickutils) - (:export)) (defpackage :scully.zdd (:use @@ -26,12 +18,11 @@ :losh :iterate :cl-arrows + :hamt :trivia :trivialib.bdd :scully.quickutils) - (:export) - (:shadowing-import-from :trivialib.bdd - :make-set)) + (:export)) (defpackage :scully.reasoners.prolog (:use diff -r d505235f4520 -r 7fe3a52bf1f6 scully.asd --- a/scully.asd Wed Nov 02 13:21:21 2016 +0000 +++ b/scully.asd Sat Nov 05 12:22:36 2016 +0000 @@ -17,6 +17,7 @@ :cl-algebraic-data-type :cl-arrows :cl-ggp + :cl-hamt :trivialib.bdd) :serial t diff -r d505235f4520 -r 7fe3a52bf1f6 src/grounders/prolog.lisp --- a/src/grounders/prolog.lisp Wed Nov 02 13:21:21 2016 +0000 +++ b/src/grounders/prolog.lisp Sat Nov 05 12:22:36 2016 +0000 @@ -2,13 +2,6 @@ ;;;; Utils -(defun fixed-point (function data &key (test 'eql)) - "Find the fixed point of `function`, starting with `data`." - (let ((next (funcall function data))) - (if (funcall test data next) - data - (fixed-point function next :test test)))) - (defun gensyms (n prefix) (iterate (repeat n) (collect (gensym prefix)))) diff -r d505235f4520 -r 7fe3a52bf1f6 src/zdd.lisp --- a/src/zdd.lisp Wed Nov 02 13:21:21 2016 +0000 +++ b/src/zdd.lisp Sat Nov 05 12:22:36 2016 +0000 @@ -463,6 +463,59 @@ (remove-if-not #'rule-ignores rules))))) +(defmethod print-object ((set hash-set) stream) + (print-unreadable-object (set stream :type t :identity nil) + (prin1 (set->list set) stream))) + +(defun hash-set= (s1 s2) + (zerop (set-size (set-symmetric-diff s1 s2)))) + +(defun rule-head-in (set rule) + (set-lookup set (rule-head rule))) + +(defun collapse-positive-heads (rules-and-heads) + (destructuring-bind (rules heads) rules-and-heads + (flet ((update-rule (rule) + (cons (rule-head rule) + (remove-if (curry #'set-lookup heads) + (rule-body rule))))) + (let* ((new-rules (set-map #'update-rule rules)) + (new-heads (-<> new-rules + (set-filter #'rule-empty-p <>) + (set-map #'rule-head <>)))) + (list (set-filter (complement (curry #'rule-head-in new-heads)) + new-rules) + (set-union heads new-heads)))))) + +(defun find-strictly-negative-rules (rules) + (set-filter (lambda (rule) + (every #'negationp (rule-body rule))) + rules)) + +(defun collapse-negative-heads (rules-and-heads) + (destructuring-bind (rules heads) rules-and-heads + (if (zerop (set-size rules)) + (list rules heads) + (labels ((negation-satisfied-p (negation) + (not (set-lookup heads (bare-term negation)))) + (rule-satisfied-p (rule) + (every #'negation-satisfied-p (rule-body rule))) + (smallest-head () + (-<> (set->list rules) + (mapcar #'rule-head <>) + (sort <> #'term<) + (first <>))) + (rules-with-head (head) + (set-filter (lambda (rule) (eql head (rule-head rule))) + rules))) + (let* ((next (smallest-head)) + (candidates (rules-with-head next))) + (list (set-diff rules candidates) + (if (some #'rule-satisfied-p (set->list candidates)) + (set-insert heads next) + heads))))))) + + (defun make-rule-tree (rules) "Create a rule tree ZDD from the given logical `rules`. @@ -537,100 +590,46 @@ ;;;; Scratch ------------------------------------------------------------------ (with-zdd - (-<> (zdd-join (zdd-family '(1 2) '(7 8) '()) - (zdd-family '(1 5 9) nil) - (zdd-set '(1))) - (print-through #'enumerate <>) - (zdd-keep-avoiders-of <> '(2 7)) - (print-through #'enumerate <>) - (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) - ) - ) - -(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 <> :unique-sinks t :unique-nodes t :hexp (curry #'<= 1000)) - ; (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) - ; ) - ) + (draw <> :unique-sinks nil :unique-nodes t + :hexp (lambda (v) (<= 1000 v))) + (never <>) + )) + +(defun test (l) + (fixed-point #'collapse-positive-heads + (list (set-insert (empty-set) + '(100 1 2) + '(1001 100 200) + '(2000 1 (not 1001)) + '(3000 1 (not 100)) + '(1 10) + '(2 30 1)) + (set-insert (empty-set :test #'eql) + '10 '20 '30)) + :limit l + :test (lambda (old new) + (and (hash-set= (first old) + (first new)) + (hash-set= (second old) + (second new)))))) -(defun test () - (with-zdd - (print-hash-table - (frequencies - (iterate (repeat 10000) - (collect (zdd-random-member - (zdd-family - '(1 2 3) - '(2) - '(1 3) - '(1 5) - '(5))))) - :test #'equal)))) - - -(with-zdd - (-<> (zdd-family - '(1 2 100 200 6000) - '(100 200 300) - '(99 100 200 300) - '(1 9900) - '() - '(1 2 1001) - ) - (mapprint-through #'enumerate <>) - (print-through '-------------- <>) - (zdd-match <> '() 100 999) - (mapprint-through #'enumerate <>) - (draw <> :hexp (lambda (v) (>= 999 v 100))) - (never <>) - )) +;;;; TODO +;; +;; * Implement head fixed-point thing for rule trees +;; * Positive head fixed-pointing +;; * Negative head fixed-pointing +;; * Fact edge case addition +;; * all (next ...) and (init ...) should have (true ...) equivalents +;; * all (legal ...) should have (does ...) equivalents +;; * Ordering for facts +;; * Base < Does < Possible < Happens +;; true does legal/term/goal sees/next +;; * Poster +;; * Monty Hall +;; * Pictures +;; * Fact sets +;; * ZDDs