; **********************************************************************
; *                                                                    *
; *  The procedures in this file filter propositional belief state     *
; *  formulae with STRIPS actions and observations.                    *
; *  They take a set of action descriptions                            *
; *  (preconditions and effects), a sequence of actions and            *
; *  observations, an initial belief state in PI-CNF (prime            *
; *  implicate CNF), a number to indicate how many                     *
; *  action/observation pairs should be filtered before subsumed       * 
; *  clauses are removed from the belief state, and a variable         *
; *  to indicate if Prime Implicates need to be found.                 *
; *  They output a belief state in PI-CNF.                             *
; *                                                                    *
; *  Author: Eyal Amir, edited by Megan Nance                          *
; *  Date:  January 7, 2003, edited September 2004                     *
; *                                                                    *
; **********************************************************************

;----------------------------------------------------------------------
		     
(defun get-list-item (identifier given-list)
  (find-if #'(lambda (x) (and (listp x) (equal identifier (car x))))
	   given-list)
)

;----------------------------------------------------------------------
;find item in the list that has as its first element identifier1 and as
;its second element identifier2.  if using substitution, nothing is 
;propositionalized yet, so we only use (car identifier2)
;         - Megan, 6/2/2004

(defun get-list-item2 (identifier1 identifier2 given-list propositional)
  (if (equal propositional 'substitution)
        (setq identifier2 (car identifier2))) 
  (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))
		    (loop for obj in (cdr formula)
			  append
			  (get-fluents obj))
		  (list formula))
	      (list formula))))
  (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).


;removes clauses from beliefState that contain any member of fluents
(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 (AND (equal (car beliefState) 'and) newbeliefState)
      (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 list-sort locallst-lit)

  (setq newlst
	(remove-duplicates ;remove-duplicates compares pairwise
	 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 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)
)

;=========================================================================
;short recursive function to apply substitution to all sublists; have to skip over 'NOT, 'OR, and 'AND 
;since those are not lists and would cause the function to error
;added by Megan, 6/3/2004

(defun subst-all (lst new old)
  (cond  
    ((NULL lst) lst)
    ((equal (car lst) NIL) (car lst))        
    ((listp (car lst))
            (if (OR (equal (caar lst) 'NOT) (equal (caar lst) 'OR) (equal (caar lst) 'AND))
                (cons (append (list (caar lst)) (subst-all (list(cadar lst)) new old) (subst-all (cddar lst) new old))
                             (append (subst-all (list (cadr lst)) new old) (subst-all (cddr lst) new old)))
                (cons (substitute new old (car lst)) (subst-all (cdr lst) new old))))
    (T (cons (substitute new old (car lst)) (subst-all (cdr lst) new old)))) 
)


;========================================================================= 

;replace gen-elements with spec-elements in lists lst1 and lst2
;gen-elements and spec-elements should be lists, where the first element
;in gen-elements should be replaced with the first element in spec-elements, 
;and so on, in both lst1 and lst2
;   -this is used instead of propositionalizing the domain
;added by Megan, 6/3/2004


(defun subst-params (spec-elements gen-elements lst1 lst2)
    (if (OR (equal (car lst1) 'AND) (equal (car lst1) 'OR)(equal (car lst1) 'NOT))
         (setq lst1front (list (car lst1)) lst1 (cdr lst1))
         (setq lst1front nil))
    (if (OR (equal (car lst2) 'AND) (equal (car lst2) 'OR) (equal (car lst1) 'NOT))
         (setq lst2front (list (car lst2)) lst2 (cdr lst2))
         (setq lst2front nil))
    
      
    (if (not (equal spec-elements nil))
        (if (eql (length spec-elements) (length gen-elements))
            (loop while spec-elements
                do
                (setq lst1 (subst-all lst1 (car spec-elements) (car gen-elements)))
                (setq lst2 (subst-all lst2 (car spec-elements) (car gen-elements)))
                (setq spec-elements (cdr spec-elements))
                (setq gen-elements (cdr gen-elements)))
            (prin1 "List lengths are not equal!")))
    (setq lst1 (append lst1front lst1))
    (setq lst2 (append lst2front lst2))
    (setq returnlst (cons lst1 lst2))
 )
;=========================================================================
;filter the beliefState using the current action and observation:
; 1-add preconditions of action "a" to beliefState
; 2-if preconditions or effects of "a" contain disjunctions, set beliefState to be the prime
;   implicates (via zres) of the cluases that contain literals from Eff(a) and
;   the clauses that do not contain literals from Eff(a)
; 3-remove clauses from beliefState that contain literals in Eff(a)
; 4-add effects of action "a" to beliefState
; 5-add the observation of "a" to beliefState
		     
(defun filter-act-obs (action observation domain beliefState propositional primeImp curr-step constraints) 
  (setq action-def (get-list-item2 ':action action domain propositional))
  (setq preconds (convert-to-CNF (get-subsequent ':precondition action-def)))  ;make sure preconds and effects are in CNF
  (setq effects (convert-to-CNF (get-subsequent ':effect action-def)))
   
  ;only before filtering over first action, if primeImp is set to T, then we will need to find
  ;  the prime implicates of the belief state, and possibly of the domain constraints
  (if (equal curr-step 1)
    (let nil
      (if primeImp 
         (setq beliefState (find-prime-imps beliefState effects)))                               ;get prime implicates of input     
      (if (AND constraints primeImp)                                                             ;if there are domain constraints, get prime implicates  
         (setq beliefState (append beliefState (list (find-prime-imps constraints effects))))))) ;  and add them to the initial belief state

    
  ;set flag to indicate if action is deterministic or not
  (if (OR (find-or effects) (find-or preconds))
     (setq deterministic-act nil)
     (setq deterministic-act T))
  
  ;if need be, substitute specific parameters into preconds and effects lists    
  (if (equal propositional 'substitution)
    (setq pre-eff (subst-params (cdr action) (cadddr action-def) effects preconds) 
            effects (car pre-eff) preconds (cdr pre-eff)))

  (if beliefState                        ;add preconditions, since we know they must be true
      (if preconds
          (if (equal (car beliefState) 'AND)
              (if (equal (car preconds) 'AND)
                (setq beliefState (append '(AND) (cdr preconds) (cdr beliefState)))
                (setq beliefState (append '(AND) (list preconds) (cdr beliefState))))
            (if (equal (car preconds) 'AND)
              (setq beliefState (append '(AND) (cdr preconds) (list beliefState)))
              (setq beliefState (append '(AND) (list preconds) (list beliefState))))))
      (if preconds
         (setq beliefState preconds)))
    
  (if (AND primeImp (NOT deterministic-act))                    ;if need be, find prime implicates after adding the preconds
     (setq beliefState (find-prime-imps beliefState effects)))  ;  if the preconds/effects are not deterministic.

  (setq beliefState (remove-clauses (get-fluents effects)beliefState))  ;remove clauses from beliefState that contain fluents
                                                        ;from the effects

  (if beliefState                        ;add effects, since we know action was successfully executed
      (if effects
          (if (equal (car beliefState) 'AND)
              (if (equal (car effects) 'AND)
                  (setq beliefState (append '(AND) (cdr effects) (cdr beliefState)))
                  (setq beliefState (append '(AND) (list effects) (cdr beliefState))))
            (if (equal (car effects) 'AND)
                (setq beliefState (append '(AND) (cdr effects) (list beliefState)))
                (setq beliefState (append '(AND) (list effects) (list beliefState))))))
      (if effects
        (setq beliefState effects)))
    
        
  (if beliefState                          ;add observation to beliefState
     (if (AND observation (NOT (EQUAL observation 'true-value)))
         (if (equal (car beliefState) 'AND)
             (if (equal (car observation) 'AND)
                 (setq beliefState (append '(AND) (cdr observation) (cdr beliefState)))
                 (setq beliefState (append '(AND) (list observation) (cdr beliefState))))
             (if (equal (car observation) 'AND)
                 (setq beliefState (append '(AND) (cdr observation) (list beliefState)))
                 (setq beliefState (append '(AND) (list observation) (list beliefState))))))
         (if (AND observation (NOT (EQUAL observation 'true-value)))
             (setq beliefState observation)))

  beliefState
)
;=========================================================================
;;if formula contains a disjunction, return that part of the formula, else return nil
(defun find-or (formula)
   (cond
        ((not formula) nil)
        ((equal formula 'OR) (list formula))
        ((listp formula)
            (cond
                ((equal (car formula) 'OR) formula)
                ((listp (car formula)) (append (find-or (car formula)) (find-or (cdr formula))))
                (T (find-or (cdr formula)))))
        (T nil)))

;=========================================================================
;;only want to find prime-imps ONCE, so make a new list that has those clauses, and remove from old list
(defun find-prime-imps (formula effects)
  ;(print formula)
   ;(print "FIND PRIME IMPLICATES")
    (setq effects (get-fluents effects))
    (setq formula-PI nil)
    (setq formula (mapc #'(lambda(x) (if (listp x)            ;;if fluents from effects and the current clause intersect, find prime implicates.
                    (if (intersection (get-fluents x)effects :test #'equal) (let nil (setq formula-PI         ;;but, if they do not intersect, we can leave
                                (append formula-PI (list x))) (delete x formula))) x)) formula)) ;;   the clause as-is
   ; (print formula-PI)
    (if formula-PI
        (setq formula (append formula (cdr (zres-PI (append '(AND) formula-PI))))))
;    (print formula-PI)
    formula)


;=========================================================================
;functions used to find prime implicates of a beliefState via zres

; 1-format is CNF input for zres
; 2-write formula to a file
; 3-call out to command line
;   will need to call:  zres (filename) -tison -timeReport # (some large #, maybe 100000)
; 4-zres will output results to: (filename).out-0.cnf
; 5-read in from file listed above, and put back into correct format
;       will need lists that tell the substitutions that were made, so can back-substitute
; 6-return list that contains formula for prime implicates (will be in CNF form)

(defun zres-PI (formula)
  ;(print "ZRES")
    (setq outfile *zres-output-path*)
   ; (print outfile)
    (setq formula (convert-to-cnf formula)) ;;put in CNF format
    (setq formula-fluents(get-fluents formula) formula-fluents2 formula-fluents)     
    (setq Xi '())
    (if (equal (car formula) 'AND)
        (setq formula (cdr formula)))        ;;remove 'AND at beginning
            
    (loop for i from 1 to (list-length formula-fluents)   ;;need to replace fluents with numbers, 
       do (setq Xi (append Xi (list i))))                 ;;so loop through to create a list of 
                                                          ;;all the numbers we will use
    (setq replace-lit (car formula-fluents))
    
    (loop for item in Xi        ;;call function to replace fluents with numbers (negated fluents are replaced with negative #'s)
        do  (setq formula (zres-replace formula item replace-lit) formula-fluents (cdr formula-fluents))               
            (setq replace-lit (car formula-fluents)))
    (zres-write formula (list-length Xi) (list-length formula))   ;;write formula to file for zres to read in


    ;(print (cons *zres-input-path* '("-tison" "-timeReport" "10000")))

    (ext:run-program *zres-path* (cons *zres-input-path* '("-tison" "-timeReport" "10000")))
    ;(print outfile)
    (setq formula-PI (read-zres formula-fluents Xi outfile))      ;;now in list format, still with numbers instead of literals

    (setq formula-fluents formula-fluents2)
    (setq replace-lit (car formula-fluents))
    (loop for item in Xi        ;;call function to replace numbers with fluents (negative #'s are replaced with negated fluents)
	  do
	  (setq formula-PI (mapcar #'(lambda(x) (setq x (zres-back-replace x replace-lit item))) formula-PI))
	  (setq formula-fluents (cdr formula-fluents))
	  (setq replace-lit (car formula-fluents)))

    (setq formula-PI (mapcar #'(lambda(x) (setq x (append '(OR) x))) formula-PI))   ;;append 'OR to each clause in formula-PI
    (setq formula-PI (append '(AND) formula-PI))
    formula-PI
)

(defun zres-replace(lst new old)
    (cond
        ((NULL lst) lst)
        ((not (listp lst))
            lst)
        ((equal (car lst) NIL) (car lst))
        ((equal (car lst) 'OR)
            ;(setq lst (cons (car lst) (zres-replace (cdr lst) new old)))
            (setq lst (zres-replace (cdr lst) new old)))
        ((equal (car lst) 'NOT)
            (if (equal (cadr lst) old)
                (setq lst (- new)))
            lst)
        ((equal lst old) new)
        (T (cons (zres-replace (car lst) new old) (zres-replace (cdr lst) new old))))) 

(defun substring (oldstring start &optional (finish -1))
     (if (< finish 0)
         (subseq oldstring start)
         (subseq oldstring start (1+ finish))
     )
)

;;function to write the formula to a file in the 
;;correct format that zres uses.
(defun zres-write (formula num-fluents num-clauses)
    (setq filename *zres-input-path*)   ;file that will later be read by zres that we will write CNF formula to
    (setq outfilestr (open filename :direction :output :if-exists :supersede :if-does-not-exist :create))
    (setq header (format nil "p cnf ~S ~S" num-fluents num-clauses))
    (write-line header outfilestr)
    
    (loop for i from 1 to num-clauses
        do (setq cur-clause (nth (- i 1) formula))
           (setq write-clause (format nil "~D" cur-clause))
           (if (listp cur-clause)
              ;(if (not (equal (length cur-clause) 1)) 
               (setq write-clause (substring write-clause 1 (- (length write-clause) 2)))write-clause)
                    ;write-clause)
           (setq write-clause (format nil "~D 0" write-clause))
           (write-line write-clause outfilestr))
    
    (close outfilestr))

(defun read-zres (fluents numbers filename)
   (setq formula-PI nil)  
   (with-open-file (stream filename :direction :input)
      (loop for line = (read-line stream nil stream)
          until (eql line stream)
            do
	    (setq start nil)
            (if (OR (<= 48 (char-int (char line 0)) 57) (equal (char line 0) '#\-))  ;;see if line begins with a number or a negative line
		(setq start 0)                                                       ;;  sometimes lines begin with spaces, so we have to account for that, too
		(if (OR (<= 48 (char-int (char line 1)) 57) (equal (char line 1) '#\-))
		    (setq start 1)))
	    (if start                 ;;if we have a number or a negative sign
               (let nil
                (setq counter start)
                (setq element nil)
                (setq clause nil)
                (setq hold nil)
                (setq str-length (length line))
                (loop
                    until (equal counter (- str-length 1))      ;;loop until we are at the end of the line
                     do
                     (if (equal (char line counter) '#\-)
                         (setq element (- (- (char-int (char line (+ 1 counter))) 48)) counter (+ 1 counter))  ;;extract number from string and negate
		       (if hold                                                                                ;;this is for numbers that are more than one digit
			   (if (< element 0)                                                                   ;;  (so, more than one character long)
                                (setq element (- (* 10 hold) (- (char-int (char line counter)) 48)) hold nil)
                                (setq element (+ (* 10 hold) (- (char-int (char line counter)) 48)) hold nil))
                            (if (not (equal (char-int (char line counter)) 32))                               ;;if not == 0 and not == whitespace(so, not at the end of a clause)
                               (setq element (- (char-int (char line counter)) 48)))))
                      (if (equal (char-int (char line counter)) 32)                       ;;if we are at a space, append the element we just pulled from the string
                            (setq counter (+ 1 counter) hold nil element nil)
                      (if (equal (char-int (char line (+ counter 1))) 32)
                          (let nil
                          (if element
                             (setq clause (append clause (list element))))
                             (setq counter (+ 1 counter))
                             (setq element nil))
                          (setq hold element counter (+ 1 counter)))))
                (setq formula-PI (append formula-PI (list clause)))))))   ;;after we go through each line, append that clause to our formula
    formula-PI)


;;recursively replace fluents with their corresponding numbers; if a fluent
;;is negated, it is replaced with the corresponding negative number
(defun zres-back-replace(lst new old)
    (setq lst (mapcar #'(lambda(x) (if (numberp x) (if (equal x old) (setq x new) 
                        (if (equal (- x) old) (setq x (append '(NOT) (list new))) x)) x)) lst))
    lst)


;---------------------------------------------------------------------------
;;;following code from:  http://norvig.com/ltd/test/cnf.lisp

;;; -*- Mode: LISP; Syntax: Common-lisp; Package: DTP; Base: 10 -*-

;;; This file was stolen from Matt Ginsberg's MVL 3/8/93

(defparameter *logical-operators* '(<= => <=> and or not))

;; stuff to manipulate propositions

;; functions defined:
;;
;; cnf (p)returns conjunctive normal form
;; dnf (p)disjunctive normal form
;; standardize-operatorsremoves => <= <=> if iff

;; conjunctive normal form.  Remove the nonstandard operators from p and
;; then look at (car p):
;;  1.  If it's NOT, then (cnf p) is the result of negating each term
;;  inside (dnf (not (p))).
;;  2.  If it's OR, then we have to combine the results of cnf'ing each
;;  of the disjuncts.  cnf-merge-lists does this, one disjunct at a
;;  time.
;;  3.  If it's AND, we just call the cnf'er and nconc the results
;;  together.
;;  4.  If it's none of these, it must be a term and we return ((p)).

;;short wrapper function to add 'AND and 'OR to list, written by Megan, 7/15/2004
(defun convert-to-cnf (p)
    (setq cnf-form (cnf p))
    (setq cnf-form (cons 'AND (mapcar #'(lambda(x) (if (NOT (equal (list-length x) 1)) (cons 'OR x) (car x))) cnf-form)))
)

(defun cnf (p)
  (case (car (setq p (standardize-operators p)))
    (not (mapcar #'(lambda (l) (mapcar #'logical-negate l)) (dnf (second p))))
    (or
      (let (ans)
	(dolist (item (cdr p) (nreverse ans))
	    (setq ans (cnf-merge-lists (cnf item) ans)))))
    (and (mapcan #'cnf (cdr p)))
    (otherwise (list (list p))))
    )

;; given a partial cnf expression d, and a new cnf exp c to be merged,
;; construct a list of all entries that have an entry from d followed by
;; one from c.  As we go through, the list is maintained backwards, so
;; that we have terms with entries late in d early in the returned
;; answer.  Three cases:
;;  1.  If c is NIL, there is nothing to do.  Return d.
;;  2.  If d is NIL, there is still nothing to do, but we reverse c to
;;  get d into "backwards" form.
;;  3.  Otherwise, work through c and for each entry in it, work through
;;  d, appending each entry of d onto that entry of c and pushing the
;;  result onto the answer being accumulated.  Note that this maintains
;;  the "backwardness" of the answer.  We make sure that each term in
;;  the final answer is a fresh copy.

(defun cnf-merge-lists (c d)
  (cond ((null c) d)
	((null d) (nreverse c))
	(t (let (ans)
	          (dolist (item c ans)
		           (push (append (car d) item) ans)
			          (dolist (x (cdr d)) (push (append x (copy-list item)) ans)))))))

;; remove nonstandard connectives from p.  Handles =>, <=, <=>, if and
;; iff.
;;  1.  (=> p1 ... pn q) means (if (and p1 ... pn) q), or
;;  (or (not (and p1 ... pn)) q).
;;  2.  (<= q p1 ... pn) means (if (and p1 ... pn) q) as well.
;;  3.  (if p q) means (or (not p) q)
;;  4.  (iff p q) means (or (and p q) (and (not p) (not q))); <=> is
;;  similar.

(defun standardize-operators (p)
  (case (car p)
    (|=>| `(or (not (and . ,(butlast (cdr p)))) ,(car (last p))))
    (|<=| `(or ,(second p) (not (and . ,(cddr p)))))
    (if `(or ,(third p) (not ,(second p))))
    ((|<=>| iff) `(or (and ,(second p) ,(third p))
		            (and ,(logical-negate (second p)) ,(logical-negate (third p)))))
    (otherwise p)))

;; dnf is a lot like cnf.

(defun dnf (p)
  (case (car (setq p (standardize-operators p)))
    (not (mapcar #'(lambda (l) (mapcar #'logical-negate l)) (cnf (second p))))
    (and
      (let (ans)
	(dolist (item (cdr p) (nreverse ans))
	    (setq ans (cnf-merge-lists (dnf item) ans)))))
    (or (mapcan #'dnf (cdr p)))
    (otherwise (list (list p)))))

(defun logical-negate (p)
  (if (eq 'not (car p)) (cadr p) (list 'not p)))

;=========================================================================

(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 subst in comb
	  do              
	  (setq curr-action
		(recursive-substitute (cadr subst)
				      (car subst)
				      curr-action)))
	(substitute (cons action-name (get-permutation comb))
		    action-name
		    curr-action))
      )
    )
  )

;=========================================================================

;propositionalize the entire domain
(defun propositionalize (domain objects)
  (loop for clause in domain
    append 
    (if (and (listp clause) (equal ':action (car clause)))
	(propositionalize-action clause objects)
      (list clause))
    )
)


;==========================================================================
;;added numSubsume parameter to tell how many action/obs pairs to filter before running Subsumption check
;;Megan 6/9/2004
(defun STRIPS-filter-ret (domainName sequenceName beliefs0Name beliefsNName propositional
                            objectsName collect-data numSubsume primeImp stateConstraints constraintsName)
  (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 sequence1 (getContent sequenceFile))
    
  (if stateConstraints          ;;if need be, get state constraints from file
       (let nil
	(setq constraintsFile (format nil "~A.pddl" constraintsName))
	(setq constraints (getContent constraintsFile)))
    (setq constraints nil))

  (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)
  (setq numFilter 0)

  (let nil ; main loop -- after all this preparation
    (setq beliefState belief0)
;	  (setq output-string *trace-output*)
;	  (setq *trace-output* outfilestr)
	
    (loop while (not (equal nil sequence1))
	  do     
	  (setq curr-step (+ 1 curr-step))      
	  (print curr-step)
	  (let nil
	    (setq action (car sequence1))
	    (setq observation (cadr sequence1))
	    (setq beliefState (filter-act-obs action observation domain beliefState propositional primeImp curr-step constraints))
            (setq numFilter (+ 1 numFilter))
	    (setq sequence1 (cddr sequence1)))
        (if (equal numFilter numSubsume)        ;see if we should run subsumption
           (setq beliefState (remove-subsumed beliefState) numFilter 0))
	  (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))))
	  ))

;  internal-time-units-per-second

  (if collect-data
      (list time-data space-data beliefState)
    beliefState)
)


;==========================================================================
;;added numSubsume parameter to tell how many action/obs pairs to filter before running Subsumption check
;;Megan 6/9/2004
(defun STRIPS-filter (domainName sequenceName beliefs0Name beliefsNName propositional objectsName numSubsume primeImp stateConstraints constraintsName)

    ;GLOBAL VARIABLES FOR ZRES
    (defvar *zres-path* "/home/eyal/eyal/ongo/kr/consequence/zres/zres" "Location of zres")
    (defvar *zres-input-path* "/home/eyal/nance/NNF/formula.cnf" "Location of input for zres")
    (defvar *zres-output-path* "/home/eyal/nance/NNF/formula.cnf.out-0.cnf" 
      "Location of output of zres, which will ALWAYS be the name of *zres-input-path* appended with .out-0.cnf")
    
    (setq beliefState (STRIPS-filter-ret domainName sequenceName beliefs0Name
                       beliefsNName propositional objectsName nil numSubsume
                       primeImp stateConstraints constraintsName))
  (setq outfile (format nil "~A.bel" beliefsNName))
  (write-to-file beliefState outfile "; Filtered belief state is presented below.~%") 
)

;======================================================================

;pass in 1)-domain file(.pddl), 2)-sequence file(.seq) that contains action/observation pairs,
;   3)-initial belief state(.bel), 4)-file to write end belief state to(.bel), 5)-variable to 
;   indicate if domain is already propositional (T), needs to be 
;   propositionalized (nil) or if substitution should be used ('substitution),
;   6)-an objects file(.obj) (if domain needs to be propositionalized), 7)-an integer
;   to indicate how many action/observation pairs should be filtered before 
;   subsumption is run on the current belief state (if pass in 0, subsumption is never run)
;   8)-a variable to indicate whether prime implicates should be found; if so, pass in T, 
;   else, pass in nil, 9)-a variable to inidicate if there are domain/state constraints; if so,
;   pass in T, else pass in nil 10)-domain/state constraints file(.pddl), if needed
;
;user will also need to define global variables, listed above in STRIPS-filter
;  these variables are used to indicate the location of zres (used to find prime implicates),
;  the location of input for zres, and the location of the zres output.


(defun main ()
  (print(time(STRIPS-filter "/home/eyal/nance/Generator/chess-domain"
      "/home/eyal/nance/Generator/generator_tests/chess50_seq3"
      "/home/eyal/nance/Generator/chess-domain"
      "/home/eyal/nance/Generator/generator_tests/output_seq1" 
      'substitution nil 10 T nil nil)))
)

(main)