# HG changeset patch # User Steve Losh # Date 1478092881 0 # Node ID d505235f4520b3b97df4f479e35733e8153e06cb # Parent 1151f5fc872ee371684fc629d1ea0fec2114a631 More documentation diff -r 1151f5fc872e -r d505235f4520 src/zdd.lisp --- a/src/zdd.lisp Wed Nov 02 12:30:21 2016 +0000 +++ b/src/zdd.lisp Wed Nov 02 13:21:21 2016 +0000 @@ -464,6 +464,17 @@ (defun make-rule-tree (rules) + "Create a rule tree ZDD from the given logical `rules`. + + `rules` should be a list of rules, each of the form: + `(head-term &rest body-terms)` + + Each head term should be a single variable. + Each body term should be either a single variable or `(not variable)`. + + Rules and bodies do not need to be sorted beforehand. + + " (recursively ((rules (mapcar #'sort-body rules)) (accumulated-heads nil)) (let* ((heads (-<> rules @@ -485,6 +496,12 @@ (defun apply-rule-tree (zdd rule-tree head-bound) + "Apply the logical rules in `rule-tree` to the sets in `zdd`. + + `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. + + " (recursively ((zdd zdd) (rule-tree rule-tree)) (ematch* (zdd rule-tree)