; ********************************************************************** ; * * ; * The procedures in this file filter a belief state (set of * ; * possible world states) represented as a formula in propositional * ; * logic with a sequence of actions and observations. * ; * These procedures take a set of action descriptions * ; * (preconditions and effects), a sequence of actions and * ; * observations, and an initial belief state in PI-CNF (prime * ; * implicate CNF). They output a belief state in PI-CNF. * ; * * ; * Author: Alex Jaffe (re-using STRIPS-filter code by Eyal Amir) * ; * Date: January 1, 2004 * ; * * ; ********************************************************************** ;Fix tilde-g as stated near the function ;This version of NNF-Filter doesn't do recursion on itself, it should be looped externally ;to filter a sequence of actions/observations (defun NNF-Filter-2 (action-observation belief preconditions effects t-value) (if (equal t-value 0) belief (let* ((cur-preconditions (append preconditions (list (make-frame preconditions)))) (cur-effects (append effects (list (make-frame preconditions)))) (B-formula (make-B (car action-observation) t-value cur-preconditions cur-effects))) (let ((big-stuff (conjunct (list (cdr action-observation) (nnf-form B-formula) (NNF-ProgressStep (car action-observation) belief preconditions effects))))) big-stuff)))) ;============================================================================== (defun make-completions-from-literal (literal preconditions effects) (if (or (equal literal 'true-value) (equal literal '(not true-value))) nil (let ((new-literal (if (negationp literal) (cadr literal) literal))) (if (member-for-subsumes new-literal (get-fluents-from-formula (conjunct effects))) (list (cons (conjunct (list literal (make-frame preconditions))) literal) (cons (conjunct (list (negate literal) (make-frame preconditions))) (logical-negate literal))) (list (cons literal literal) (cons (logical-negate literal) (logical-negate literal))))))) ;============================================================================== (defun make-frame (rules) (nnf-form (cons 'and (mapcar #'(lambda (x) (list 'not x)) rules)))) (defun nnf-form (formula) (if (literalp formula) formula (if (equal 'not (car formula)) (if (disjunctionp (cadr formula)) (conjunct (mapcar #'(lambda (x) (nnf-form (list 'not x))) (cdadr formula))) (if (conjunctionp (cadr formula)) (disjunct (mapcar #'(lambda (x) (nnf-form (list 'not x))) (cdadr formula))) (if (equal 'not (caadr formula)) (nnf-form (cadadr formula))))) (if (disjunctionp formula) (disjunct (mapcar #'(lambda (x) (nnf-form x)) (cdr formula))) (conjunct (mapcar #'(lambda (x) (nnf-form x)) (cdr formula))))))) ;============================================================================== (defun NNF-ProgressStep (action belief preconditions effects) (if (literalp belief) (let* ((cur-completions (make-completions-from-literal belief preconditions effects)) (preconditions-with-completions (if cur-completions (append preconditions (list (caar cur-completions) (caadr cur-completions))) preconditions)) (effects-with-completions (if cur-completions (append effects (list (cdar cur-completions) (cdadr cur-completions))) effects)) (cur-preconditions (append preconditions-with-completions (list (make-frame preconditions)))) (cur-effects (append effects-with-completions (list (make-frame preconditions))))) (let nil (let ((progressed (progress1 action belief cur-preconditions))) (if (not progressed) 'true-value (let ((output (nnf-form (conjunct (mapcar #'(lambda (x) (disjunct (at-indices x cur-effects 1))) progressed))))) output))))) (if (disjunctionp belief) (let nil (nnf-form (disjunct (mapcar #'(lambda (x) (NNF-ProgressStep action x preconditions effects)) (cdr belief))))) (if (conjunctionp belief) (nnf-form (conjunct (mapcar #'(lambda (x) (NNF-ProgressStep action x preconditions effects)) (cdr belief)))) (error "Input to nnf-progressstep not a literal, disjunction or conjunction."))))) ;============================================================================== ;LOGICAL HELPERS ;All helpers operate under the assumption of only three logical operators in use: 'and, 'or, and 'not. ;All helpers work on literal lists, for example, '(big lump of clay) is an appropriate atom, as is 'clay. This is because all helpers assume compound expressions will include ands, ors, and nots. However, this means that all literal names cannot include the reserved words 'and, 'or, and 'not. '(big and tall) is not an appropriate atom. '(and big tall) IS an appropriate logical expression. ;PROC INTERFACE: Negate takes a belief, and lists the word 'not with that belief. DOES NOT adjoin 'not to a list, that wouldn't make any sense. (defun negate (term) (list 'not term)) ;PROC INTERFACE: logical-negate takes a belief, and negates it, cancelling them if two outer 'not exist. (defun logical-negate (term) (if (and (listp term) (equal (car term) 'not)) (cadr term) (list 'not term))) ;PROC INTERFACE: Conjunct and disjunct take a list of beliefs and adjoin the work 'and or 'or to the front of the list. (defun conjunct (items) (cons 'and items)) (defun disjunct (items) (cons 'or items)) ;PROC INTERFACE: Conjunct-literal and disjunct-literal take a fluent instead of a list of expressions, and negate it by listing it with 'not. (defun conjunct-literal (item) (list 'and item)) (defun disjunct-literal (item) (list 'or item)) ;PROC INTERFACE: literalp takes any literal value and returns true iff it is not a conjunction, a disjunction, a negation of a conjunction, or a negation of a disjunction. thus all inputs that literalp returns true on should be atoms or negations of atoms. Does not crash on improperly formed input. (defun literalp (formula) (if (consp formula) (if (or (equal (car formula) 'and) (equal (car formula) 'or)) nil (if (equal (car formula) 'not) (if (atomp (cadr formula)) (not nil) nil) (not nil))) (not nil))) ;PROC INTERFACE: disjunctionp and conjunction p take any literal expression, and return true if it is a disjunction or conjunction, respectively. Does not crash on improperly formed inputs. (defun disjunctionp (formula) (if (not (consp formula)) nil (equal (car formula) 'or))) (defun conjunctionp (formula) (if (not (consp formula)) nil (equal (car formula) 'and))) (defun negationp (formula) (if (not (consp formula)) nil (equal (car formula) 'not))) ;PROC INTERFACE: atomp takes in any literal expression and returns true if it is an atom. That is, if it is not a conjunction, disjunction, or negation. (defun atomp (formula) (or (not (consp formula)) (and (not (equal (car formula) 'not)) (not (equal (car formula) 'and)) (not (equal (car formula) 'or))))) ;PROC INTERFACE: Comes from earlier code with comments gone. (defun get-fluents-from-formula (formula) (setq fluents (if formula (if (listp formula) (if (or (equal (car formula) 'and) (equal (car formula) 'or) (equal (car formula) 'not)) (loop for obj in (cdr formula) append (get-fluents-from-formula obj)) (list formula)) (list formula)))) (remove-duplicates fluents :from-end T :test #'equal) ) ;PROC INTERFACE: nnf-to-dnf and nnf-to-cnf take in a negation-normal-form logical expression, including no empty conjunctions or disjunctions. Returns a cnf or dnf formula that is logically equivalent. ;INTENDED USE: to simplify filtered expressions when outputted. (defun nnf-to-cnf (formula) (if (cnfp-formatted formula) formula (if (conjunctionp formula) (flatten-ands (conjunct (mapcar #'nnf-to-cnf (cdr formula)))) (if (disjunctionp formula) (nnf-to-cnf (distr-disj (disjunct (flatten-ors formula)))) formula)))) (defun nnf-to-dnf (formula) (if (dnfp-formatted formula) formula (if (disjunctionp formula) (disjunct (flatten-ors (disjunct (mapcar #'nnf-to-dnf (cdr formula))))) (if (conjunctionp formula) (nnf-to-dnf (distr-conj (flatten-ands formula))) formula)))) ;PROC INTERFACE: dnfp-formatted and cnfp-formatted are predicates that take in a (well-formed) logical expression, and return true iff it is in dnf or cnf form. Will work correctly on badly formed expressions. (defun cnfp-formatted (formula) (cond ((conjunctionp formula) (null (remove-if #'(lambda (x) (and (not (conjunctionp x)) (cnfp-formatted x))) (cdr formula)))) ((disjunctionp formula) (null (remove-if #'(lambda (x) (and (not (disjunctionp x)) (not (conjunctionp x)) (cnfp-formatted x))) (cdr formula)))) ((not nil)))) (defun dnfp-formatted (formula) (cond ((disjunctionp formula) (null (remove-if #'(lambda (x) (and (not (disjunctionp x)) (dnfp-formatted x))) (cdr formula)))) ((conjunctionp formula) (null (remove-if #'(lambda (x) (and (not (conjunctionp x)) (not (disjunctionp x)) (dnfp-formatted x))) (cdr formula)))) ((not nil)))) ;remove-subsumed-from-dnf seems to work on cnf expressions as well! This happens because we are assuming the formulas are cnf or dnf. Subsumes-p was meant to work on conjunctions in a disjunction, where a larger one is subsumed by a subset, but this is also true of disjunctions in a conjunction. ;PROC INTERFACE: remove-subsumed-from-dnf takes in the cdr of a dnf-formatted logical expression. That is, it takes a list of conjunctions. It returns a new list of conjunctions in which some of the conjunctions are removed. A conjunction is removed if it is logically subsumed by another conjunction. ;INTENDED USE: to simplify a filtered expression before output, after it has been converted to dnf. The 'or must be stripped off before being passed to remove-subsumed-from-dnf, and must be put back on the returned list in the calling function. (defun remove-subsumed-from-dnf (formula) (let ((undupe (remove-duplicates-for-subsumes formula))) (cons (car undupe) (remove-subsumed-helper (cdr undupe) (cdr undupe))))) (defun remove-subsumed-helper (formula result) (if (not formula) result (if (member-for-subsumes (car formula) result) (let ((cur-removed (remove-if #'(lambda (x) (and (not (equal x (car formula))) (subsumes-p (car formula) x))) result))) (remove-subsumed-helper (cdr formula) cur-removed)) (remove-subsumed-helper (cdr formula) result)))) ;PROC INTERFACE: remove-duplicates-for-subsumes removes duplicate expressions from a list of expressions. ;INTENDED USE: to remove the duplicates conjunctions in a list that is the cdr of a dnf expression, before subsumed clauses are removed (this function is called by remove-subsumed-from-dnf). Written to take advantage of member-for-subsumes, which compares sublists, not just atomic literals. (defun remove-duplicates-for-subsumes (formula) (if (not formula) formula (if (member-for-subsumes (car formula) (cdr formula)) (remove-duplicates-for-subsumes (cdr formula)) (cons (car formula) (remove-duplicates-for-subsumes (cdr formula)))))) ;PROC INTERFACE: subsumes-p takes in a subsumer expression and a subsumed expression, that are both assumed to be conjunctions of literals. Returns true if subsumer subsumes subsumed, that is, if subsumer's literals are a subset of subsumed's literals. Returns false if subsumer and subsumed are equal, because we want to remove duplicates from lists of expressions separately. (defun subsumes-p (subsumer subsumed) (if (not subsumer) nil (if (literalp subsumer) (if (literalp subsumed) nil (member-for-subsumes subsumer subsumed)) (if (literalp subsumed) nil (if (not (cddr subsumer)) ;we know its and and before this (member-for-subsumes (cadr subsumer) subsumed) (if (member-for-subsumes (cadr subsumer) subsumed) (subsumes-p (conjunct (cddr subsumer)) subsumed) nil)))))) ;PROC INTERFACE: member-for-subsumes compares sublists, not just atomic literals. So '(not b) gives yes for '(a (not b))) ;INTENDED USE: for any time we need to check if a list is in another list, specifically useful for remove-duplicates-for-subsumed. (defun member-for-subsumes (exp1 exp2) (if (not exp2) nil (if (equal exp1 (car exp2)) (not nil) (member-for-subsumes exp1 (cdr exp2))))) ;FLATTEN-ANDS WORKS DIFFERENTLY THAN FLATTEN-ORS! IT RETURNS A CONJUNCTION, NOT A LIST THAT NEEDS TO BE CONJUNCTED AFTERWARDS! ;PROC INTERFACE: flatten-ands takes in a logical expression. If it is not a conjunction, it returns it immediately. If it is a conjunction of no arguments, it will error (hopefully these will never be passed around). Otherwise, it's a conjunction of at least one argument, in which case we flatten all top-level depths of 'ands. For example: flatten-ands on '(and 3 (or (and 5 6) 7) (and 8 (and 9 (hey there))) (and (watch out) 12) 13 (not (and 14 15)) (not (or 16 17))) returns '(and 3 (or (and 5 6) 7) 8 9 10 11 12 13 (not (and 14 15)) (not (or 16 17))). Note that flatten-ands does NOT distribute disjunctions or conjunctions through negations. ALSO note that flatten-ands takes in a full conjunction (or something else), not a lists of expressions, and returns a full conjunction (or something else), not a list of expressions. (defun flatten-ands (formula) (cond ((not (conjunctionp formula)) formula) ((not (cdr formula)) nil) ((conjunctionp (cadr formula)) (append (flatten-ands (cadr formula)) (cdr (flatten-ands (conjunct (cddr formula)))))) ((conjunct (cons (cadr formula) (cdr (flatten-ands (conjunct (cddr formula))))))))) ;============================================================================= (defun remove-true-values (formula) (if (literalp formula) formula (if (conjunctionp formula) (let ((new-formula (remove-if #'(lambda (y) (equal y 'true-value)) (conjunct (mapcar #'(lambda (x) (remove-true-values x)) (cdr formula)))))) (if (not (cdr new-formula)) ;all clauses in and have been removed 'true-value (if (member-for-subsumes '(not true-value) new-formula) '(not true-value) new-formula))) (if (disjunctionp formula) (let ((new-formula (remove-if #'(lambda (y) (equal y '(not true-value))) (disjunct (mapcar #'(lambda (x) (remove-true-values x)) (cdr formula)))))) (if (not (cdr new-formula)) ;all clauses in and have been removed '(not true-value) (if (member-for-subsumes 'true-value new-formula) 'true-value new-formula))))))) ;PROC INTERFACE: Takes in a well-formed nnf logical expression, and returns a significantly more compact version by removing trues and falses, switching to dnf, removing duplicate sub-clauses from each clause, and removing clauses that are subsumed by one another. ;It's possible that some of the following steps are redundant. (defun multi-stage-simplify-cnf-4 (formula) (if (atomp formula) formula (let* ((stage1 (remove-true-values formula)) (stage2 (nnf-to-cnf stage1)) (stage3 (conjunct (mapcar #'(lambda (x) (if (or (not (listp x)) (atomp x)) x (remove-duplicates-for-subsumes x))) (remove-if #'(lambda (x) (includes-tautology x)) (cdr stage2))))) (stage4 (remove-subsumed-from-dnf stage3))) stage4))) ;PROC INTERFACE: Returns true if list of elements includes an atom and its negation (defun includes-tautology (lst) (if (not lst) nil (let ((car-inverted (if (negationp (car lst)) (cadar lst) (list 'not (car lst))))) (or (member-for-subsumes car-inverted (cdr lst)) (includes-tautology (cdr lst)))))) ;============================================================================== ;Takes a literal, negated or non, and an NNF formula. Returns true or false ;depending on whether the literal entails the formula. (defun literal-entailsp (literal formula) (if (tautologyp formula) (not nil) (if (literalp formula) (equal formula literal) ;else its a conjunction or disjunction (if (conjunctionp formula) (equal (find-if #'(lambda (x) (not (literal-entailsp literal x))) formula) nil) (if (find-if #'(lambda (x) (not (literalp x))) formula) (literal-entailsp (distr-disj formula)) (not (equal (find-if #'(lambda (x) (literal-entailsp literal x)) formula) nil))))))) (defun distr-disj (formula) (let ((result formula) (flag nil)) (do ((tempy (cdr formula) (cdr tempy))) (flag result) (if (not tempy) (let nil (if (disjunctionp result) (setq result (disjunct (flatten-ors result)))) (setq flag (not nil))) (if (not (or (literalp (car tempy)) (disjunctionp (car tempy)))) (let nil (setq result (cons (car tempy) (remove-if #'(lambda (x) (equal x (car tempy))) (cdr formula)))) (setq result (cons (caar result) (mapcar #'(lambda (x) (disjunct (cons x (cdr result)))) (cdar result)))) (setq flag (not nil)))))))) ;FIX THIS! Does not work on '(and a b), where there are no ors!, but distr-disj does work on similar thing. What's the difference? (defun distr-conj (formula) (let ((result formula) (flag nil)) (do ((tempy (cdr formula) (cdr tempy))) (flag result) (if (not tempy) (let nil (if (conjunctionp result) (setq result (flatten-ands result))) (setq flag (not nil))) (if (not (or (literalp (car tempy)) (conjunctionp (car tempy)))) (let nil (setq result (cons (car tempy) (remove-if #'(lambda (x) (equal x (car tempy))) (cdr formula)))) (setq result (cons (caar result) (mapcar #'(lambda (x) (conjunct (cons x (cdr result)))) (cdar result)))) (setq flag (not nil)))))))) ;============================================================================== (defun tautologyp (formula) (equal 'true-value (ttl-entails 'true-value formula))) (defun new-memq (check-for lst) (if (not lst) nil (if (equal check-for (car lst)) (not nil) (new-memq check-for (cdr lst))))) ;correct one, works only on disjunctions of two or more from high level. (defun flatten-ors (formula) (if (disjunctionp formula) (if (not (cdr formula)) nil (append (flatten-ors (cadr formula)) (flatten-ors (cons 'or (cddr formula))))) (if (not formula) formula (list formula)))) (defun flatten (tree) (if (not (consp tree)) (if (not tree) tree (list tree)) (append (flatten (car tree)) (flatten (cdr tree))))) ;============================================================================= ;PROGRESS1 COMPONENTS ;frame rule should already be present ;only returns numbers ;write completion function! ;put in completions, either unioning them with each subset, or taking subsets partially from them. (defun progress1 (action formula preconditions) (setq disjunctions nil) (setq indices (mapcar #'(lambda (x) (list x)) (make-sequence-from-list 1 (length preconditions)))) (setq not-entailed (list (remove-if #'(lambda (x) (if (equal 'true-value (ttl-entails formula (nth (- (car x) 1) preconditions))) (setq disjunctions (append disjunctions (list x))))) indices))) (do ((size 2 (+ 1 size))) ((> size (length preconditions)) disjunctions) (setq poss-sets (sat-size (car (last not-entailed)) size)) (setq cur-not-entailed (list (remove-if #'(lambda (x) (if (equal 'true-value (ttl-entails formula (disjunct (at-indices x preconditions 1)))) (setq disjunctions (append disjunctions (list x))))) poss-sets))) (setq not-entailed (append not-entailed cur-not-entailed)))) ;takes ordered lists ;make work with size parameter 2 (defun sat-size (anti-ent size) (let ((not-entailed anti-ent)) (let ((new-values nil)) (if (equal size 1) not-entailed ;(if (orderedp not-entailed) ;else order, assume for now it is already (do ((holder1 not-entailed (cdr holder1))) ((not holder1) new-values) ;nil is temporary (do ((holder2 (cdr holder1) (cdr holder2))) ((not holder2) nil) ;nil is temporary (let ((combo (ordered-union (car holder1) (car holder2)))) (if (not (find-if #'(lambda (x) (equal combo x)) new-values)) (if (equal (length combo) size) (if (tuples-in-listp combo not-entailed (- size 1)) (setq new-values (append new-values (list combo))))))))))))) (defun tuples (set size) (if (equal (length set) size) (list set) (append (tuples-helper set size) (tuples (cdr set) size)))) (defun tuples-helper (set size) (if (equal size 1) (list (list (car set))) (if (not set) nil (if (equal (length set) size) (list set) (if (< (length set) size) nil (remove-if #'(lambda (x) (not x)) (mapcar #'(lambda (x) (cons (car set) x)) (tuples (cdr set) (- size 1))))))))) ;can return 'entails-positive 'entails-negative or 'entails-nothing ;made for nnf-form, I believe (defun ttl-entails (formula question) (setq current-truth nil) (setq truth nil) (setq flag nil) (setq fluents (unordered-union (get-fluents-from-formula formula) (get-fluents-from-formula question))) (setq truth-table (make-table)) (setq truth-table (populate-truthtable truth-table fluents formula question)) (setq table-size (expt 2 (length fluents))) ;everything should be true or false in table (do ((count 1 (+ count 1))) (truth truth) ;remember to set flag in last case (let nil (if (> count table-size) (if (not current-truth) (setq truth 'entails-nothing) (setq truth current-truth)) (let ((formula-value (lookup-two count formula truth-table)) (question-value (lookup-two count question truth-table))) (if (equal formula-value 'true-value) (if (not current-truth) (setq current-truth question-value) (if (equal question-value 'false-value) (if (equal current-truth 'true-value) (setq truth 'entails-nothing) (if (equal question-value 'true-value) (if (equal current-truth 'false-value) (setq truth 'entails-nothing)))))))))))) (defun remove-nots (lst) (if (not lst) lst (if (equal (car lst) 'not) (remove-nots (cdr lst)) (cons (car lst) (remove-nots (cdr lst)))))) ;assumes that form and q are composed solely of the symbols in sym. Can do error-checking later. (defun populate-truthtable (tbl sym form q) (do ((count 1 (+ count 1))) ((> count (expt 2 (length sym))) tbl) (let ((bin (binary-num (- count 1) (length sym)))) (mapcar #'(lambda (x y) (insert-two count x (truth-name y) tbl)) sym bin) (insert-two count form (get-truth form (lookup-one count (cdr tbl))) tbl) (insert-two count q (get-truth q (lookup-one count (cdr tbl))) tbl) nil))) (defun truth-name (num) (if (equal 1 num) 'true-value (if (equal 0 num) 'false-value))) (defun binary-num (number digits) (if (equal digits 1) (if (> number 0) (list 1) (list 0)) (if (> (+ number 1) (expt 2 (- digits 1))) (cons 1 (binary-num (- number (expt 2 (- digits 1))) (- digits 1))) (cons 0 (binary-num number (- digits 1)))))) (defun get-truth (form vals) (if (equal form 'true-value) 'true-value (if (equal form 'false-value) 'false-value (if (literalp form) (if (atomp form) (lookup-one form vals) (if (equal (lookup-one (cadr form) vals) 'true-value) 'false-value 'true-value)) (if (equal (car form) 'not) (let ((tal (get-truth (cadr form) vals))) (if (equal tal 'false-value) 'true-value (if (equal tal 'true-value) 'false-value))) (if (disjunctionp form) (if (find-if #'(lambda (x) (equal 'true-value (get-truth x vals))) (cdr form)) 'true-value 'false-value) (if (find-if #'(lambda (x) (equal 'false-value (get-truth x vals))) (cdr form)) 'false-value 'true-value))))))) (defun tuples-in-listp (set lst size) (not (find-if #'(lambda (x) (not (find-if #'(lambda (y) (equal x y)) lst))) (tuples set size)))) ;===================================================================================== ;adapted from structure and interpretation of computer programs ;works for unlabed tables (defun lookup-one (key table) (let ((record (associat key table))) (if record (cdr record) nil))) (defun associat (key records) (if (equal nil records) nil (if (equal key (caar records)) (car records) (associat key (cdr records))))) ;must set-cdr somehow, not setq of cdr (defun insert-one (key value table) (let ((record (associat key (cdr table)))) (if record (setf (cdr record) value) (setf (cdr table) (cons (cons key value) (cdr table))))) 'ok) (defun make-table () (list 'table)) ; two-dimensional (defun lookup-two (key-1 key-2 table) (let ((subtable (associat key-1 (cdr table)))) (if subtable (let ((record (associat key-2 (cdr subtable)))) (if record (cdr record) nil)) nil))) (defun insert-two (key-1 key-2 value table) (let ((subtable (associat key-1 (cdr table)))) (if subtable (let ((record (associat key-2 (cdr subtable)))) (if record (setf (cdr record) value) (setf (cdr subtable) (cons (cons key-2 value) (cdr subtable))))) (setf (cdr table) (cons (list key-1 (cons key-2 value)) (cdr table))))) 'ok) ;===================================================================================== ;SET COMBINATION FUNCTIONS FOR SET TESTING IN NNF-PROGRESS (defun unordered-union (set1 set2) (setq result (copy-seq set2)) (setq copy-set (copy-seq set1)) (do ((locale copy-set (cdr locale))) ((not locale) result) (if (not (member (car locale) set2)) (setq result (cons (car locale) result))))) (defun ordered-union-two (set1 set2) (sort (unordered-union set1 set2))) (defun ordered-union (set1 set2) (setq result (copy-seq set2)) (setq copy-set (copy-seq set1)) (do ((locale copy-set (cdr locale))) ((not locale) (sort result #'<)) (if (not (member (car locale) set2)) (setq result (cons (car locale) result))))) ;assumes index from 1 (defun at-indices (indices items cur-index) (if (equal items nil) nil (if (equal (car indices) cur-index) (cons (car items) (at-indices (cdr indices) (cdr items) (+ cur-index 1))) (at-indices indices (cdr items) (+ cur-index 1))))) (defun make-B (action number preconditions effects) (if (not preconditions) 'true-value (let ((result1 (make-B-part1 preconditions effects number)) (result2 (make-B-part2 preconditions effects number action))) ;check to see if make-b-part2 has anything to work with, starts with t+1 (if (>= number (length preconditions)) result1 (conjunct (list result1 result2)))))) ;When given a shorter first sequence, the second will be appropriately ;lengthed as well. (defun make-B-part1 (preconds effects number) (cons 'and (mapcar (lambda (x y) (list 'or (list 'not x) y)) (subseq preconds 0 number) effects))) (defun make-subsets-from-list (lst) (if (not (cdr lst)) (list lst) (let ((lower (make-subsets-from-list (cdr lst)))) (cons (list (car lst)) (append (mapcar #'(lambda (x) (cons (car lst) x)) lower) lower))))) (defun make-sequence-from-list (start end) (if (not (> start end)) (cons start (make-sequence-from-list (+ start 1) end)))) ;just takes a list of preconds from 1 to l, with the final being m+1. (defun make-B-part2 (preconds effects number action) (let ((sets (make-subsets-from-list (make-sequence-from-list (+ number 1) (length preconds))))) (conjunct (make-B-part2-helper preconds effects number sets)))) (defun make-B-part2-helper (preconds effects number some-sets) (let ((all-results nil)) (do ((one-set some-sets (cdr one-set))) ((not one-set) all-results) (let ((tilg (make-tilde-G2 (car one-set) number effects preconds))) (let ((current (if (not tilg) (disjunct (list (disjunct (at-indices (car one-set) effects 1)))) (disjunct (list tilg (disjunct (at-indices (car one-set) effects 1))))))) (setq all-results (append all-results (list current)))))))) ;Changed on August 21, had forgotten the else case!!! (defun remove-subset (this from) (if (not this) from (if (member (car this) from) (remove-subset (cdr this) (remove-if #'(lambda (x) (equal (car this) x)) from)) (remove-subset (cdr this) from)))) ;;Almost all of tilde-g is right, but right now on the last line, it is only testing entailment of the literals themselves that are in not-eff-a. We're supposed to be testing expressions in the language of the literals. (defun make-tilde-G (set number effects preconditions) (let* ((eff-a (remove-nots (flatten (get-fluents-from-formula effects)))) (not-eff-a (remove-subset eff-a (remove-nots (flatten (get-fluents-from-formula preconditions))))) main-formula (conjunct (mapcar #'(lambda (x) (list 'not x)) (at-indices set preconditions 1))))) (remove-if #'(lambda (x) (not (equal 'true-value (ttl-entails main-formula x)))) not-eff-a)) ; 'tilde-g) (defun make-tilde-G2 (set number effects preconditions) (let* ((eff-a (remove-nots (flatten (get-fluents-from-formula effects)))) (not-eff-a (remove-subset eff-a (remove-nots (flatten (get-fluents-from-formula preconditions))))) (main-formula (conjunct (mapcar #'(lambda (x) (list 'not x)) (at-indices set preconditions 1)))) (the-cons (find-consequences main-formula not-eff-a 1 '()))) (if the-cons (conjunct the-cons) 'true-value))) ;PROC INTERFACE: find-consequences takes in a well-formed logical expression (formula), a list of atoms (language), a current-disjunction-length, and an iterative result list of consequences (current-list). (defun find-consequences (formula language current-disjunction-length current-list) ; if current-disjunction-length is greater than length of language (if (> current-disjunction-length (length language)) ; then return current-list current-list ; else generate list of disjunctions of current-disjunction-length from list of literals (considering negations as well) (let* ((cur-lists (generate-disjunctions language current-disjunction-length)) ; Remove those disjunctions which are subsumed by one in current-list of lesser length (cur-disj (mapcar #'disjunct cur-lists)) (subs-free (remove-if #'(lambda (x) (not (not (remove-if #'(lambda (y) (subsumes-p y x)) current-list)))) cur-disj)) ; remove those disjunctions which are not entailed by formula (entailed-only (remove-if #'(lambda (x) (not (equal 'true-value (ttl-entails formula x)))) subs-free))) ; append list onto current-list as argument to find-consequences, with current-disjunction-length incremented (find-consequences formula language (+ 1 current-disjunction-length) entailed-only)))) ;Works except needs to fill in the formula column, by processing the truth value of the formula in each case. At lesat now the literals and their negations are filled in in a proper way, with all possible values. (defun make-ffpi-table (formula language) (let* ((num-fluents (length language)) (num-columns (+ 1 (* 2 num-fluents))) ;there is a column for each literal, negation, and 1 formula (num-rows (+ 1 (expt 2 num-fluents))) (full-table (make-array (list num-rows num-columns)))) ;just filling non-negated literals first, formula goes in column 0 (setf (aref full-table 0 0) formula) (do ((cur-col 1 (+ cur-col 1))) ((> cur-col num-fluents) nil) (setf (aref full-table 0 cur-col) (nth (- cur-col 1) language)) (setf (aref full-table 0 (+ num-fluents cur-col)) (list 'not (aref full-table 0 cur-col)))) (do ((cur-row 1 (+ cur-row 1))) ((> cur-row (- num-rows 1)) full-table) (let ((binary-number-left (- cur-row 1))) (let ((cur-power-of-two (expt 2 (- num-fluents 1)))) ;this is the value of the first col (do ((cur-col 1 (+ cur-col 1))) ((> cur-col num-fluents) nil) (if (> binary-number-left (- cur-power-of-two 1)) ;if this spot should have a true/one. (let nil (setf (aref full-table cur-row cur-col) 'true-value) ;set fluent (setf (aref full-table cur-row (+ cur-col num-fluents)) 'false-value) ;set negation (setf binary-number-left (- binary-number-left cur-power-of-two)) (setf cur-power-of-two (/ cur-power-of-two 2))) (let nil (setf (aref full-table cur-row cur-col) 'false-value) ;set fluent (setf (aref full-table cur-row (+ cur-col num-fluents)) 'true-value) ;set negation (setf cur-power-of-two (/ cur-power-of-two 2))))))) (setf (aref full-table cur-row 0) (get-truth formula (make-key-value-bindings-from-ffpi-table full-table 1 num-fluents cur-row)))))) ;PROC INTERFACE: safe-length is to be used when the argument may be a singe word, and we want to return a length of one in that case. (defun safe-length (x) (if (listp x) (length x) 1)) ;This is the difficult problem of knowing how to get clauses of length > 2 without generating unnecessary ones. Oh well, for now will generate all clauses of length n out of fluents that aren't themselves implicates. Then will check if subsumed by implicates larger than one by cycling through. (defun make-new-ffpi-table (old-table implicates-so-far length-to-compute non-implicate-fluents) ;Create a list of implicates in standard form that are of correct length, constructed out of non-implicate fluents (let ((test-implicates (generate-disjunctions non-implicate-fluents length-to-compute)) (old-number-of-columns (array-dimension old-table 1)) (number-of-no-negation-fluents (+ (length non-implicate-fluents) (length (remove-if #'(lambda (x) (> (safe-length x) 1)) implicates-so-far))))) ;Go through each longer implicate from implicates-so-far, removing all formulae they subsume from the list (mapcar #'(lambda (x) (setf test-implicates (remove-if #'(lambda (y) (subsumes-p x y)) test-implicates)) x) (remove-if #'(lambda (x) (= (safe-length x) 1)) implicates-so-far)) ;we know that length 1's won't subsume, also test subsumesp ;add on to old table a number of columns equal to length of list (adjust-array old-table (list (array-dimension old-table 0) (+ (length test-implicates) (array-dimension old-table 1)))) ;fill names of clauses (let ((number-of-test-implicates (length test-implicates))) (do ((cur-col 0 (+ cur-col 1))) ((> (+ 1 cur-col) number-of-test-implicates) nil) (setf (aref old-table 0 (+ cur-col old-number-of-columns)) (nth cur-col test-implicates)))) ;fill truth-values of each clause given literals (do ((cur-row 1 (+ cur-row 1))) ((> (+ 1 cur-row) (array-dimension old-table 0)) nil) ;THIS IS THE PROBLEM BELOW I tried turning number-of-no-negation-fluents into array dimension to just get all the values ;since you don't know which number-of-no... fluents are going to be the ones (let ((bindings-for-this-row (make-key-value-bindings-from-ffpi-table old-table 1 (- (array-dimension old-table 1) 1) cur-row))) (do ((cur-col old-number-of-columns (+ cur-col 1))) ((> (+ 1 cur-col) (array-dimension old-table 1)) nil) (setf (aref old-table cur-row cur-col) (get-truth (disjunct (aref old-table 0 cur-col)) bindings-for-this-row))))))) (defun make-key-value-bindings-from-ffpi-table (table start last row) (if (> start last) nil (cons (cons (aref table 0 start) (aref table row start)) (make-key-value-bindings-from-ffpi-table table (+ start 1) last row)))) (defun get-falses-from-column (table number) (let ((list-of-indices nil)) (do ((cur-row (- (array-dimension table 0) 1) (- cur-row 1))) ((> 1 cur-row) list-of-indices) ;shouldn't look at top row; it contains formulae (if (equal 'false-value (aref table cur-row number)) (setf list-of-indices (cons cur-row list-of-indices)) nil)))) (defun fpi (arg) (fast-find-prime-implicates-proper-output arg)) ;NEED TO PROCESS OUTPUT BY TURNING IT INTO A CONJUNCTION OF DISJUNCTIONS!!! ;fix so that even single-fluent implicates go in the list of implicates as one-element lists (defun fast-find-prime-implicates-proper-output (formula) (let* ((language (get-fluents-from-formula formula)) (working-table (make-ffpi-table formula language))) ;0th column (2nd dimension) will contain formula truth-value (let ((all-prime-implicates '()) (api-no-formatting '()) (non-implicate-fluents '()) (list-of-falses (get-falses-from-column working-table 0))) (let ((cur-col-to-check-prime-implicate 1)) (do ((current-clause-length 1 (+ current-clause-length 1))) ;this loop goes through each size of clause to be checked ((not list-of-falses) (conjunct all-prime-implicates)) ;hopefully when no falses are left, all the pi's will imply the formula. ;end if after a particular clause length we have all prime implicates (let nil (do () ;this loop goes through each clause of current size, working with an index that remains throughout outer loop ((or (> (+ cur-col-to-check-prime-implicate 1) (array-dimension working-table 1)) (not list-of-falses)) nil) (let nil (print "in inner loop") (if (formula-implies working-table cur-col-to-check-prime-implicate) ;since we know formula will be in col 0, no arg nec (let ((zeroes-in-cur-col (unused-zeroes-in-col working-table cur-col-to-check-prime-implicate list-of-falses))) ;above finds the zeroes in the column which are still needed to finish implication (if zeroes-in-cur-col (let nil (setf list-of-falses (remove-if #'(lambda (x) (member x zeroes-in-cur-col)) list-of-falses)) (setf all-prime-implicates (cons (if (= current-clause-length 1) (disjunct-literal (name-of-implicate working-table cur-col-to-check-prime-implicate)) (disjunct (name-of-implicate working-table cur-col-to-check-prime-implicate))) all-prime-implicates)) (setf api-no-formatting (cons (name-of-implicate working-table cur-col-to-check-prime-implicate) api-no-formatting))) ;update the falses that we are still looking for, and the implicates we've found (stored in well-formed form) nil)) nil) (setf cur-col-to-check-prime-implicate (+ 1 cur-col-to-check-prime-implicate)))) (if (= current-clause-length 1) ;do a special check so that we have this information available later for generating tables (setf non-implicate-fluents (remove-subset (mapcar #'(lambda (x) (if (negationp (cadr x)) (cadr (cadr x)) (cadr x))) all-prime-implicates) language)) nil) (make-new-ffpi-table working-table api-no-formatting (+ 1 current-clause-length) non-implicate-fluents) (if (< current-clause-length 5) (print working-table) nil) )))))) (defun unused-zeroes-in-col (table number falses-still-needed) (let ((all-falses-from-col (get-falses-from-column table number))) (intersection falses-still-needed all-falses-from-col))) (defun name-of-implicate (table column) (aref table 0 column)) (defun formula-implies (table column) (let ((flag (not nil))) (do ((cur-row (- (array-dimension table 0) 1) (- cur-row 1))) ((> 1 cur-row) flag) ;shouldn't look at top row; it contains formulae (if (equal 'true-value (aref table cur-row 0)) (if (not (equal 'true-value (aref table cur-row column))) (let nil (setf flag nil) (setf cur-row 0)) nil) nil)))) ;PROC INTERFACE: Takes in a list of symbols that constitute a language, and a length of disjunctions to generate from it. Returns a list of all sensible length-element lists of atoms in the language or negations of atoms in the language. Should be turned into disjunctions externally. (defun generate-disjunctions (language length) (if (> length (length language)) nil (if (not language) nil (if (equal length 1) (append (mapcar #'(lambda (x) (list x)) language) (mapcar #'(lambda (x) (list (list 'not x))) language)) (let ((same-length-rest (generate-disjunctions (cdr language) length)) (shorter-rest (generate-disjunctions (cdr language) (- length 1)))) (let ((me-shorter (mapcar #'(lambda (x) (cons (car language) x)) shorter-rest)) (not-me-shorter (mapcar #'(lambda (x) (cons (list 'not (car language)) x)) shorter-rest))) (append me-shorter not-me-shorter same-length-rest))))))) ;============================================================================== ;from here on, taken from pre-existing code by Eyal Amir ;========================================================================= ; ********************************************************************** ; * * ; * The procedures in this file filter propositional STRIPS actions * ; * and observations. They take a set of action descriptions * ; * (preconditions and effects), a sequence of actions and * ; * observations, and an initial belief state in PI-CNF (prime * ; * implicate CNF). They output a belief state in PI-CNF. * ; * * ; * Author: Eyal Amir * ; * Date: January 7, 2003 * ; * * ; ********************************************************************** ;---------------------------------------------------------------------- (defun get-list-item (identifier given-list) (find-if #'(lambda (x) (and (listp x) (equal identifier (car x)))) given-list) ) ;---------------------------------------------------------------------- (defun get-list-item2 (identifier1 identifier2 given-list) (find-if #'(lambda (x) (and (listp x) (equal identifier1 (car x)) (equal identifier2 (cadr x)))) given-list) ) ;---------------------------------------------------------------------- (defun get-list-item-rest (identifier given-list) (remove-if #'(lambda (x) (and (listp x) (equal identifier (car x)))) given-list) ) ;---------------------------------------------------------------------- (defun recursive-substitute (new-item old-item tree) (if tree ; else nil (if (not (listp tree)) (if (equal old-item tree) new-item tree) ; stop (cons (recursive-substitute new-item old-item (car tree)) (recursive-substitute new-item old-item (cdr tree))) ) )) ;---------------------------------------------------------------------- (defun mod1 (x m) (+ 1 (mod (- x 1) m)) ) ;---------------------------------------------------------------------- (defun list-to-string (lst) (if lst ; otherwise, return nil (if (cdr lst) ; if list has more than one item (format nil "~A~A" (write-to-string (car lst)) (list-to-string (cdr lst))) (write-to-string (car lst))) ; if list has length 1 ) ) ;---------------------------------------------------------------------- (defun get-subsequent (start lst) (nth (+ 1 (position start lst)) lst) ) ;---------------------------------------------------------------------- (defun get-literals (formula) (setq literals (if formula ; else nil (if (listp formula) (if (or (equal (car formula) 'and) (equal (car formula) 'or)) (get-literals (cdr formula)) (if (listp (car formula)) (append (get-literals (car formula)) (get-literals (cdr formula))) (list formula))) (if (not (or (equal formula 'and) (equal formula 'or) (equal formula 'variable))) (list formula)) ; else nil ) )) (remove-duplicates literals :from-end T :test #'equal) ) ;---------------------------------------------------------------------- (defun get-fluents (formula) (setq fluents (if formula ; else nil (if (listp formula) (if (or (equal (car formula) 'and) (equal (car formula) 'or) (equal (car formula) 'not)) (get-fluents (cdr formula)) (if (listp (car formula)) (append (get-fluents (car formula)) (get-fluents (cdr formula))) (list formula))) (if (not (or (equal formula 'and) (equal formula 'or) (equal formula 'not))) (list formula)) ; else nil ) )) (remove-duplicates fluents :from-end T :test #'equal) ) ;---------------------------------------------------------------------- (defun find-recursive (fluents clause) (if clause (if (not (listp clause)) (if (find clause fluents) T nil) (if (or (find-recursive fluents (car clause)) (find-recursive fluents (cdr clause))) T nil) ) ) ) ;---------------------------------------------------------------------- ; We implemented this as a loop because it turns up being a very long ; recursion, even for moderate numbers of fluents (~400), which in turn ; breaks some lisp implementations. ; Alas, the recursive version (below) is faster, but unstable (for now). (defun remove-clauses (fluents beliefState) (setq bs0 beliefState) (setq newBeliefState nil) (loop while bs0 do (if (and (not (equal (car bs0) 'and)) (not (intersection fluents (get-fluents (car bs0)) :test #'equal))) ; add this clause only if no fluent ; from the list appears in the clause. (setq newBeliefState (cons (car bs0) newBeliefState))) (setq bs0 (cdr bs0)) ) (if (equal (car beliefState) 'and) (setq newBeliefState (cons 'and newBeliefState))) newBeliefState ) ;---------------------------------------------------------------------- ;(defun remove-clauses (fluents beliefState) ; (if (equal beliefState nil) nil ; (append ; (if (equal (car beliefState) 'and) '(and) ; (if (intersection fluents (get-fluents (car beliefState)) ; :test #'equal) ; nil ; (list (car beliefState))) ; ) ; (remove-clauses fluents (cdr beliefState))) ; ) ; ) ;---------------------------------------------------------------------- ; group-literals: append the list of literals to each clause in lst (defun group-literals (lst) (if lst (cons (list (car lst) (get-literals (car lst))) (group-literals (cdr lst)))) ) ;---------------------------------------------------------------------- (defun get-clauses (lst) (if lst (cons (caar lst) (get-clauses (cdr lst))) ) ) ;---------------------------------------------------------------------- (defun remove-subsumed (lst) (if (member 'and lst) (let nil (setq locallst (remove 'and lst :test #'equal)) (setq myAnd 'and)) (let nil (setq myAnd nil) (setq locallst lst))) (setq locallst-lit (group-literals locallst)) (setq newlst (remove-duplicates locallst-lit :from-end T :test #'(lambda (x y) (subsetp (cadr x) (cadr y) :test #'equal)))) (setq newlst (get-clauses newlst)) (if myAnd (cons myAnd newlst) newlst) ) ;---------------------------------------------------------------------- (defun add-clauses (beliefState1 beliefState2) (setq beliefState (remove-subsumed (append beliefState1 beliefState2))) ) ;========================================================================= (defun getContent (filename) (setq filestr (open filename :direction :input)) (format *standard-output* "reading file : ~S~%" filename) (setq content (read filestr)) ; reads a list from the file (close filestr) content ) ;========================================================================= (defun write-to-file (lst filename comment) (setq outfilestr (open filename :direction :output :if-exists :supersede :if-does-not-exist :create)) (format outfilestr comment) (prin1 lst outfilestr) (close outfilestr) ) ;========================================================================= (defun append-to-file (filename comment) (setq outfilestr (open filename :direction :output :if-exists :append :if-does-not-exist :create)) (format outfilestr comment) (close outfilestr) ) ;========================================================================= ;(defun filter-act (action domain beliefState) ; (setq action-def (get-list-item2 ':action action domain)) ; (setq preconds (get-subsequent ':precondition action-def)) ; (setq effects (get-subsequent ':effect action-def)); ; (setq effA (get-fluents effects)) ; (setq preA (get-fluents preconds)) ; (setq beliefState (remove-clauses effA beliefState)) ; (setq beliefState (add-clauses effects beliefState)) ;) ;========================================================================= (defun filter-obs (observation beliefState) (add-clauses observation beliefState) ; **** change to complete prime implicates and remove subsumed clauses (can avoid this as long as observations are single literals ) ;========================================================================= (defun all-permutations (variables objects) (if (equal nil variables) (list nil) (let ((var nil)) (setq var (car variables)) (setq permutations-togo (all-permutations (cdr variables) objects)) (loop for obj in objects append (loop for perm in permutations-togo collect (cons (list var obj) perm))) ) ) ) ;========================================================================= (defun get-permutation (combination) (loop for item in combination collect (cadr item)) ) ;========================================================================= (defun propositionalize-action (action-def objects) (let ((action-name nil) (params nil) (preconds nil) (effects nil)) (setq action-name (cadr action-def)) (setq params (get-subsequent ':parameters action-def)) (setq preconds (get-subsequent ':precondition action-def)) (setq effects (get-subsequent ':effect action-def)) (setq combinations (all-permutations params objects)) (loop for comb in combinations collect (let ((curr-action action-def)) (loop for substitution in comb do (setq curr-action (recursive-substitute (cadr substitution) (car substitution) curr-action))) (substitute (cons action-name (get-permutation comb)) action-name curr-action)) ) ) ) ;========================================================================= (defun propositionalize (domain objects) (loop for clause in domain append (if (and (listp clause) (equal ':action (car clause))) (propositionalize-action clause objects) (list clause)) ) ) ;====================================================================== ;This section by Alex Jaffe (defun fix-sequence (seq) (if (not seq) seq (if (not (cdr seq)) (cons (car seq) 'true-value) (if (not (cadr seq)) (cons (cons (car seq) 'true-value) (fix-sequence (cddr seq))) (cons (cons (car seq) (cadr seq)) (fix-sequence (cddr seq))))))) (defun sequence-preconditions (seq domain) (if (not seq) seq (let nil ;(car seq) is the first action in the sequence (setq action-def (get-list-item2 ':action (car seq) domain)) (setq precond (get-subsequent ':precondition action-def)) (cons (list precond) (sequence-preconditions (cddr seq) domain))))) (defun sequence-effects (seq domain) (if (not seq) seq (let nil ;(car seq) is the first action in the sequence (setq action-def (get-list-item2 ':action (car seq) domain)) (setq effect (get-subsequent ':effect action-def)) (cons (list effect) (sequence-effects (cddr seq) domain))))) ;========================================================================== (defun NNF-filter-ret (domainName sequenceName beliefs0Name beliefsNName propositional objectsName collect-data) (setq domainFile (format nil "~A.pddl" domainName)) (setq sequenceFile (format nil "~A.seq" sequenceName)) (setq beliefs0File (format nil "~A.bel" beliefs0Name)) (setq domain (getContent domainFile)) (setq belief0 (getContent beliefs0File)) (setq sequence (getContent sequenceFile)) (if (not propositional) (let nil (setq objectsFile (format nil "~A.objs" objectsName)) (setq objects (getContent objectsFile)) (setq domain (propositionalize domain objects)) (prin1 "Finished propositionalization of domain") )) (if collect-data (let nil (setq time-data nil) (setq space-data nil) )) ; (get-universal-time) (setq start-time (get-internal-real-time)) (setq curr-step 0) (let nil ; main loop -- after all this preparation (setq beliefState belief0) ; (setq output-string *trace-output*) ; (setq *trace-output* outfilestr) (setq our-seq (fix-sequence sequence)) (setq our-seq-preconditions (sequence-preconditions sequence domain)) (setq our-seq-effects (sequence-effects sequence domain)) ;nnf-filter will take in an action, a belief state, a list of preconditions for that action, a list of effects for that action, a number t for what number we're currently on, last filter (loop while (not (equal nil our-seq)) do (setq curr-step (+ 1 curr-step)) (let nil (setq action-observation (car our-seq)) (setq this-action-preconditions (car our-seq-preconditions)) (setq this-action-effects (car our-seq-effects)) (setq beliefState (nnf-filter-2 action-observation beliefState this-action-preconditions this-action-effects curr-step)) (setq beliefState (multi-stage-simplify-cnf-4 beliefState)) (setq beliefState (fast-find-prime-implicates-proper-output beliefState)) (setq our-seq (cdr our-seq)) (setq our-seq-preconditions (cdr our-seq-preconditions)) (setq our-seq-effects (cdr our-seq-effects))) (if collect-data (let nil (setq time-per-step (round (/ (- (get-internal-real-time) start-time) curr-step))) (setq time-data (cons time-per-step time-data)) (setq space-data (cons (list-length beliefState) space-data)))) )) (if collect-data (list time-data space-data beliefState) beliefState) ) ;========================================================================== (defun STRIPS-filter (domainName sequenceName beliefs0Name beliefsNName propositional objectsName) (setq beliefState (STRIPS-filter-ret domainName sequenceName beliefs0Name beliefsNName propositional objectsName nil)) (setq outfile (format nil "~A.bel" beliefsNName)) (write-to-file beliefState outfile "; Filtered belief state is presented below.~%") ) (defun NNF-filter-shell (domainName sequenceName beliefs0Name beliefsNName propositional objectsName) (setq beliefState (NNF-filter-ret domainName sequenceName beliefs0Name beliefsNName propositional objectsName nil)) (setq outfile (format nil "~A.bel" beliefsNName)) (write-to-file beliefState outfile "; Filtered belief state is presented below.~%") ) (defun main-single () (NNF-filter-shell "blocks-domain" "ijcai03-exper-dir/ijcai03-exper/blocks-rand-seq3x10" "blocks-begin" "ijcai03-exper-dir/ijcai03-exper/blocks-end3x10" nil "ijcai03-exper-dir/ijcai03-exper/blocks-inst3") ) ;====================================================================== (defun random-sequence (domainName length propositional objectsName outFileName) (setq domainFile (format nil "~A.pddl" domainName)) (setq domain (getContent domainFile)) (if (not propositional) (let nil (setq objectsFile (format nil "~A.objs" objectsName)) (setq objects (getContent objectsFile)) (setq domain (propositionalize domain objects)) (prin1 "Finished propositionalization of domain") )) (setq action-num (- (length domain) 4)) ; *** Should be made more general (setq sequence (loop for i from 1 to length append (list (cadr (nth (+ 4 (random action-num)) domain)) nil) ; creates an action and observation, with nil observations )) (setq outfile (format nil "~A.seq" outFileName)) (write-to-file sequence outfile "; Random action/observation sequence is presented below.~%") ) ;====================================================================== (defun main-prop-single () (NNF-filter-shell "blocks-prop-domain" "blocks-sequence-prop" "blocks-begin" "blocks-end-prop" t nil) ) ;====================================================================== (defun main-random (num-objects) (setq old-trace-output *trace-output*) (loop for i in '(10 20 30 40 50 60 70 80 90 100 120 140 160 180 200 250 300 350 400 450 500 600 700 800 900 1000) do (setq randSeqFile (format nil "ijcai03-exper/blocks-rand-seq~Ax~A" num-objects i)) (setq blocksInstFile (format nil "ijcai03-exper/blocks-inst~A" num-objects)) (setq blocksEndFile (format nil "ijcai03-exper/blocks-end~Ax~A" num-objects i)) (random-sequence "blocks-domain" i nil blocksInstFile randSeqFile) (setq outfile (format nil "~A.bel" blocksEndFile)) (setq outfilestr (open outfile :direction :output :if-exists :supersede :if-does-not-exist :create)) (format outfilestr "; Filtered belief state for domain ~A with ~A object after ~A actions/observations is presented below.~%" "blocks-domain" num-objects i) (setq *trace-output* outfilestr) (setq beliefState (STRIPS-filter-ret "blocks-domain" randSeqFile "blocks-begin" blocksEndFile nil blocksInstFile nil)) ; timed inside (format outfilestr "~%") (prin1 beliefState outfilestr) (close outfilestr) (format t "Finished processing ~A~%" randSeqFile) ) (setq *trace-output* old-trace-output) ) ;====================================================================== (defun breadth-exper (seq-len) (setq old-trace-output *trace-output*) (loop for num-objects from 3 to 20 do (setq randSeqFile (format nil "ijcai03-breadth/blocks-rand-seq~Ax~A" num-objects seq-len)) (setq blocksInstFile (format nil "ijcai03-exper/blocks-inst~A" num-objects)) (setq blocksEndFile (format nil "ijcai03-breadth/blocks-end~Ax~A" num-objects seq-len)) (random-sequence "blocks-domain" seq-len nil blocksInstFile randSeqFile) (setq outfile (format nil "~A.bel" blocksEndFile)) (setq outfilestr (open outfile :direction :output :if-exists :supersede :if-does-not-exist :create)) (format outfilestr "; Filtered belief state for domain ~A with ~A object after ~A actions/observations is presented below.~%" "blocks-domain" num-objects seq-len) (setq *trace-output* outfilestr) (setq beliefState (STRIPS-filter-ret "blocks-domain" randSeqFile "blocks-begin" blocksEndFile nil blocksInstFile nil)) ; timed inside (format outfilestr "~%") (prin1 beliefState outfilestr) (close outfilestr) (format t "Finished processing ~A~%" randSeqFile) ) (setq *trace-output* old-trace-output) ) ;====================================================================== (defun single-exper (num-objects seq-len) (setq old-trace-output *trace-output*) (setq randSeqFile (format nil "ijcai03-breadth/blocks-rand-seq~Ax~A" num-objects seq-len)) (setq blocksInstFile (format nil "ijcai03-exper/blocks-inst~A" num-objects)) (setq blocksEndFile (format nil "ijcai03-breadth/blocks-end~Ax~A" num-objects seq-len)) (random-sequence "blocks-domain" seq-len nil blocksInstFile randSeqFile) (setq outfile (format nil "~A.bel" blocksEndFile)) (setq outfilestr (open outfile :direction :output :if-exists :supersede :if-does-not-exist :create)) (format outfilestr "; Filtered belief state for domain ~A with ~A object after ~A actions/observations is presented below.~%" "blocks-domain" num-objects seq-len) (setq *trace-output* outfilestr) (setq beliefState (STRIPS-filter-ret "blocks-domain" randSeqFile "blocks-begin" blocksEndFile nil blocksInstFile nil)) ; timed inside (format outfilestr "~%") (prin1 beliefState outfilestr) (close outfilestr) (format t "Finished processing ~A~%" randSeqFile) (setq *trace-output* old-trace-output) ) ;====================================================================== (defun single-collect-random (num-objects seq-len) (setq old-trace-output *trace-output*) (setq randSeqFile (format nil "ijcai03-exper3/blocks-rand-seq~Ax~A" num-objects seq-len)) (setq blocksInstFile (format nil "ijcai03-domains/blocks-inst~A" num-objects)) (setq blocksEndFile (format nil "ijcai03-exper3/blocks-end~Ax~A" num-objects seq-len)) (random-sequence "blocks-domain" seq-len nil blocksInstFile randSeqFile) (setq outfile (format nil "~A.bel" blocksEndFile)) (setq outfilestr (open outfile :direction :output :if-exists :supersede :if-does-not-exist :create)) (format outfilestr "; Filtered belief state for domain ~A with ~A object after ~A actions/observations is presented below.~%" "blocks-domain" num-objects seq-len) ; (setq *trace-output* outfilestr) ; (setq *trace-output* nil) (setq filter-pack (STRIPS-filter-ret "blocks-domain" randSeqFile "blocks-begin" blocksEndFile nil blocksInstFile T)) ; timed inside (setq time-data (car filter-pack)) (setq space-data (cadr filter-pack)) (setq beliefState (caddr filter-pack)) (format outfilestr "; Time per step~%") (prin1 time-data outfilestr) (format outfilestr "~%; Space (#literals) per step~%") (prin1 space-data outfilestr) (format outfilestr "~%; Final belief state~%") (prin1 beliefState outfilestr) (close outfilestr) (format t "Finished processing ~A~%" randSeqFile) ; (setq *trace-output* old-trace-output) ) ;====================================================================== (defun main () (STRIPS-filter "blocks-domain" "ijcai03-exper/blocks-rand-seq3x10" "blocks-begin" "ijcai03-exper/blocks-end3x10" nil "ijcai03-exper/blocks-inst3") ) ;====================================================================== (defun main-collect () (loop for num-objects from 3 to 20 do (single-collect-random num-objects 4000) ) )