;;;===========================================================================
;;;
;;;
;;;                               R W M
;;;
;;;               R e f i n e m e n t  W i t h  M a c r o s
;;;
;;;
;;;                       by  H. Altay Guvenir
;;;
;;;===========================================================================

(in-package "USER")

;; Top-level functions of rwm

(setq *print-pretty* nil)
(setq *load-verbose* nil)

;; Initialize PROBLEMS, a global variable.
(defun i (&rest file-name-arg)
  (declare (special PROBLEMS NAME GOAL FILE-NAME print-stage))
  (let ((prob nil))
    (cond ((null file-name-arg)		;problem file name is not specified
	   (write-string "Problem: ") (read-line)
	   (setq FILE-NAME (read-line)))
	  (t (setq FILE-NAME (car file-name-arg))))
    (setq prob (initialize FILE-NAME))
    (of nil)
    (of (list `("Problem: 0 stage: 0 and 1 are initialized to:" 
		,(concatenate 'string "\"" NAME "\""))))
    (setq PROBLEMS (list (list (list NAME GOAL) prob)))
    (of nil)))


;; Show the sn_th stage of pn_th problem.

(defun s (pn sn)
  (declare (special PROBLEMS))
  (of (list `("Problem:" ,pn "stage:" ,sn "is:")))
  (print-stage (nth sn (nth pn PROBLEMS))))


;; Refine the sn_th stage of pn_th problem

(defun r (pn sn)
  (declare (special PROBLEMS))
  (prog (new-stages)
	(setq new-stages (refine (nth sn (nth pn PROBLEMS))))
	(of (list `("Problem:" ,pn "stage:" ,sn "refined into"
			      ,(length new-stages) "subproblems")))
	(nconc new-stages (nthcdr (1+ sn) (nth pn PROBLEMS)))
	(rplacd (nthcdr (1- sn) (nth pn PROBLEMS)) new-stages)
	(of nil)))


;; Show the status of the pn_th problem

(defun p (pn)
  (declare (special PROBLEMS))
  (of (list `("Problem:" ,pn ,(car (nth 0 (nth pn PROBLEMS))))
	    `("Goal is:" ,(cadr (nth 0 (nth pn PROBLEMS))))))
  (of nil)
  (of (list `("Strategy is:")))
  (do ((stages (cdr (nth pn PROBLEMS)) (cdr stages))
       (sn 1))
      ((null stages))
      (of (list `("Stage no:" ,sn))) (setq sn (1+ sn))
      (print-stage (car stages))))


;; Make macros for the sn_th stage of pn_th problem

(defun m (pn sn)
  (declare (special PROBLEMS))
  (prog (new-macros)
	(setq new-macros (make-macros (nth sn (nth pn PROBLEMS))))
	(of (list `("Problem:" ,pn "stage:" ,sn ,(length new-macros)
			     "new moves are generated")))
	(of (list `("updated stages:"
			    ,(update-strategy (nthcdr sn (nth pn PROBLEMS))
					      new-macros))))
	(of nil)))


;; Exit
(defun x ()
  (declare (special PROBLEMS OPERATORS MACROS))
  (of (list `("Processor Time:" 
	      ,(round (get-internal-run-time) internal-time-units-per-second)
	      "sec.")))
  (of (list `(,(- (apply #'+ (mapcar #'(lambda (x) (length (cdr x)))
				     MACROS))
		  (length OPERATORS))
	      "macros are generated")))
  (of nil)
  (do ((problems PROBLEMS (cdr problems))
       (pn 0 (1+ pn)))
      ((null problems))
      (p-rm-cyc pn))   ; print the stages by removing possible cycles 
  (of (list `("Processor Time:" 
	      ,(round (get-internal-run-time) internal-time-units-per-second)
	      "sec."))))


;; Create a subproblem (subgoaling) for a move mv in sn_th stage of pn_th prob.

(defun c (pn sn mv)
  (declare (special PROBLEMS))
  (prog (move title subp)
	(setq move (assoc mv (nth 2 (nth sn (nth pn PROBLEMS))) 
			  :test #'equal))
	(of (list `("Problem:" ,pn "stage:" ,sn "move:" ,(car move))
		  `(,(cdr move))))
	(setq title (list `("Precondition for" 
			    ,(apply 'concatenate 
				    (cons 'string 
					  (mapcar 'write-to-string 
						  (car move)))))
			  (cadr move)))
	(setq subp `(,(cadr move)
		     ,(nth 1 (nth sn (nth pn PROBLEMS)))
		     ,@(get-moves (nth 1 (nth sn (nth pn PROBLEMS)))
				  (nth 1 move)
				  (nth 2 (nth sn (nth pn PROBLEMS)))
				  (nth 3 (nth sn (nth pn PROBLEMS))))))
	(of (list `("problem no:" ,(length PROBLEMS) "is created")))
	(rplacd (last PROBLEMS)	(list (list title subp)))
	(of nil)))


;; initializes the rwm to the problem whose description is given in "infile",
;; returns the problem initialized.

(defun initialize (infile)
  (declare (special DDKB CONSTANTS VARIABLES PREDICATES
		    INITIAL CURRENT GOAL OPERATORS MACROS))
  (progn
    (load (concatenate 'string  "PROBLEMS/" infile))
    (load (concatenate 'string "DDKB/" DDKB))
    (setq GOAL (mapcan 'expand-pred GOAL))
    (setq OPERATORS (mapcar 'allign OPERATORS))
    (setq INITIAL (mapcan 'expand-pred INITIAL))
    (setq MACROS nil) (mapcar 'add-new-macro OPERATORS)
    (setq CURRENT (mapcar #'(lambda (v) (cons v (mapcar 'list PREDICATES)))
			  (append CONSTANTS VARIABLES)))
    (add-stmt INITIAL CURRENT)
    (add-stmt (for-all-S 'NE CONSTANTS) CURRENT)
    ; return the problem
    (list GOAL         ; Target
	  CURRENT      ; Current (Initial)
	  OPERATORS    ; Relevant Moves 
	  nil)))       ; Irrelevant Moves


;; returns a list of distinct moves with respect to "statement".

(defun distinct-moves (statement moves)
  (do ((distinct-ones (list (car moves)))
       (moves (cdr moves) (cdr moves)))
      ((null moves) distinct-ones)
      (setq distinct-ones
	    (add-if-distinct (car moves) distinct-ones statement))))

;; "move" will be added to "moves" if it is distinct
;; if not, and shorter than its equivalent, it will replace its equivalent.

(defun add-if-distinct (move moves statement)
  (do ((check moves (cdr check)))
      ((null check) ; move is distinct
       (rplacd (last moves) (list move)) moves)
      (cond ((and (eq-effect-moves (car check) move statement)
		  (eq-set (cadar check) (cadr move)))  ; compare pcs
	     ; move and (car check) are equivalent, choose the shortest
	     (cond ((< (length (car move)) (length (caar check)))
		    (rplaca check move)))
	     (return moves)))))

;; Show the status of the pn_th problem and 
;; remove the cycles in the move names

(defun p-rm-cyc (pn)
  (declare (special PROBLEMS))
  (of (list `("Problem:" ,pn ,(car (nth 0 (nth pn PROBLEMS))))
	    `("Goal is:" ,(cadr (nth 0 (nth pn PROBLEMS))))))
  (of nil)
  (of (list `("Strategy is:")))
  (do ((stages (cdr (nth pn PROBLEMS)) (cdr stages))
       (sn 1))
      ((null stages))
      (of (list `("Stage no:" ,sn))) (setq sn (1+ sn))
      (print-stage-rm-cyc (car stages))))


;; Prints the given "stage" in Short format.
;; Only the names of the distinct relevant moves are printed.
;; Cycles are not removed by default.

(defun print-stage-rm-cyc (stage)
  (of `(,(list "Target:"  (nth 0 stage)) ; Target Statement
	,(cons "Moves:"			 ; Relevant Moves
	       (mapcar 'pr-mv
		       (mapcar #'(lambda (m) (rm-cycles m (nth 1 stage)))
			       (distinct-moves (nth 0 stage)
					       (nth 2 stage)))))))
  (of nil))


;; removes the cycles from move "long-m".
(defun rm-cycles (long-m p-list)
  (declare (special OPERATORS))
  (do ((long-indx (cdar long-m) (cdr long-indx)) ; names of the moves
       (all (list (assoc (list (caar long-m)) OPERATORS)))
       (short (assoc (list (caar long-m)) OPERATORS :test #'equal))
       (test))
      ((null long-indx) short)
      (setq test (extend short
			 (assoc (list (car long-indx)) OPERATORS :test #'equal)
			 p-list))
      (cond ((null (cddr test))
	     (return (rm-cycles (cons (cdr long-indx) (cdr long-m)) p-list))))
      (do ((all-indx all (cdr all-indx)))
	  (nil)
	  (cond ((equal (cdr test) (cdar all-indx))
		 (rplacd all-indx nil)
		 (setq short (car all-indx))
		 (return))
		((null (cdr all-indx))
		 (rplacd all-indx (list test))
		 (setq short test)
		 (return))))))
	    
 
;; Returns a list of two list,first being the set of relevant moves for
;;"target",and the second the irrelevant moves.This function is used to
;;get the relevant and irrelevant moves for a precondition statement in
;; creating a subgoal.

(defun get-moves (current target rel-moves irr-moves)
  (mapcar 'nconc
	  (part-rel-irr rel-moves target current)
	  (part-rel-irr irr-moves target current)))
	

;; a stage made from "row-stage".

(defun make-stage (row-stage)
  (list (caadr   row-stage)    ; target
	(car     row-stage)    ; current
	(cadadr  row-stage)    ; relevant moves
	(caddr (cadr row-stage))))  ; irrelevant moves


;; Prints the given "stage" in Short format.
;; Only the names of the distinct relevant moves are printed.

(defun print-stage (stage)
  (of `(,(list "Target:"  (nth 0 stage)) ; Target Statement
	,(cons "Moves:"		  	 ; Relevant Moves
	       (mapcar 'pr-mv
		       (distinct-moves (nth 0 stage)
				       (nth 2 stage))))))
  (of nil))


(defun pr-mv (move)
  (list (read-from-string (apply 'concatenate (cons 'string (mapcar 'write-to-string (car move)))))))
  

;; Every stage is updated with the list of "new-moves".
;; Returns a list with same number of elements as "strategy". 
;; An element is "t" if the corresponding stage has been updated.

(defun update-strategy (strategy new-moves)
  (mapcar #'(lambda (stage)
	      (update-stage stage new-moves))
	  strategy))

(defun update-stage (stage new-moves)
  (do ((moves new-moves (cdr moves))
       (updated))
      ((null moves) updated)
      (cond ((and (safe (car moves) (nth 1 stage))
		  (or (null (cadar moves))   ; no precondition
		      (pt-applicable (car moves) (nth 1 stage))))
	     ; (car moves) is good, update rels and irrs of the stage
	     (setq updated t)
	     (cond ((relevant (car moves) (nth 0 stage) (nth 1 stage))
		    (nconc (nth 2 stage) (list (car moves))))
		   (t ; irrelevant
		    (nconc (nth 3 stage) (list (car moves)))))))))


	     





;;---------------------------------------------------------------------
;; REFINER FUNCTIONS
;;---------------------------------------------------------------------

;; partitions the "safe-moves" into relevant and irrelevant moves
;; for each a-statement of "target".

(defun find-rels (target current safe-moves)
  (let ((a-statements (mapcar 'list target)))
    (do ((a-stmts a-statements (cdr a-stmts)))
	((null a-stmts) a-statements)
	(nconc (car a-stmts)
	       (part-rel-irr safe-moves (car a-stmts) current)))))
;; returns a list of
;; ((a-statement)
;;  (list of relevant moves)
;;  (list of irrelevant moves))


;; groups the a-stmts of "a-stmt-rels" with same relevant moves
;; into one statement.

(defun group-a-stmts (a-stmt-rels)
  (do ((a-stmts-o a-stmt-rels (cdr a-stmts-o))
       (groups) (statement))
      ((null a-stmts-o) groups)        ; end of outer loop
      (setq statement (list (caar a-stmts-o))) ; initialize the statement
      (do ((a-stmts-i (cdr a-stmts-o) (cdr a-stmts-i)))
	  ((null a-stmts-i))    ; end of inner loop
	  (cond ((eq-moves (cadar a-stmts-o) (cadar a-stmts-i)) ; compare rels
		 ; combine the a-stmts of inner to the statement
		 (rplacd (car a-stmts-i) nil)
		 (nconc statement (car a-stmts-i))
		 ; update the outer loop
		 (setq a-stmts-o (delete (car a-stmts-i) a-stmts-o)))))
      ; change the statement of (car a-stmts-o)
      (rplaca (car a-stmts-o) statement)
      ; add it to the list of groups
      (setq groups (cons (car a-stmts-o) groups))))
;;  Returns a list of GROUPs, where
;;  a GROUP is
;;            ((a group of a-statements)
;;             (their relevant moves   )
;;             (their irrelevant moves ))


;; t if the names of "move-list-1" and "move-list-2" are equal
;; compares only by the names

(defun eq-moves (move-list-1 move-list-2)
  (do ((list-1 move-list-1 (cdr list-1))
       (list-2 move-list-2 (cdr list-2)))
      ((and (null list-1) (null list-2)) t)
      (cond ((not (equal (caar list-1) (caar list-2))) (return nil)))))


;; partitions "s-moves" into (rel-moves irr-moves).

(defun part-rel-irr (s-moves target current)
  (do ((moves s-moves (cdr moves))
       (rel-moves) (irr-moves))
      ((null moves) (list rel-moves irr-moves))
      (cond ((relevant (car moves) target current)
	     (setq rel-moves (nconc rel-moves (list (car moves)))))
	    (t
	     (setq irr-moves (nconc irr-moves (list (car moves))))))))


;; returns the refined problem.

(defun refine (problem)
  (let ((target    (nth 0 problem))
	(current   (nth 1 problem))
	(safe-moves (append (nth 2 problem) (nth 3 problem))))
    (mapcar 'make-stage 
	    (refine-rec target current safe-moves safe-moves))))

    
;; returns alist of stages, or nil if "problem" is not solvable.
;; it is Recursive.

(defun refine-rec (target current safe-moves moves)
  (prog (a-stmt-rels groups)
	(setq a-stmt-rels (find-rels target current safe-moves))
;(mapcar '(lambda (x) (of (list (car x) (mapcar 'car (cadr x))))) a-stmt-rels)
	(cond ((do ((a-s-r a-stmt-rels (cdr a-s-r)))
		   ((null a-s-r) t)     ; every a-statement has relevant moves
		   (cond ((null (nth 1 (car a-s-r)))
			  ; (car a-s-r) has no relelevant moves
			  (return nil)))))
	      (t (return nil)))         ; EXIT, problem is UNSOLVABLE
	(setq groups (group-a-stmts a-stmt-rels))
        (setq groups (reverse groups))
	(cond ((= (length groups) 1)	; there is only one group, 
	       (return (list (list current (car groups)))))) ; EXIT with IT
	(of (list `("There are" ,(length groups) "groups")))
	; Sort the groups by the no of safe-to-be moves, highest being first
	(setq groups (sort-groups groups current safe-moves))
;(mapcar '(lambda (x) (of (list (car x) (mapcar 'car (nth 1 x)) (mapcar 'car (nth 2 x)) (mapcar 'car (nth 3 x))))) groups)
	(return
	 (do ((selections groups (cdr selections))
	      (selection) (nw-tar) (nw-cur) (rest))
	     ((null selections)    ; No refinement can be done
	      (of nil)
	      (list (list current
			  (cons target
				(part-rel-irr safe-moves target current)))))
	     (setq selection (car selections)) ; try doing selection first
	     (of (list `("selection is" ,(car selection))))
	     (setq nw-tar (set-difference target (nth 0 selection) :test #'equal))
	     (setq nw-cur (add-stmt (nth 0 selection) (copy-tree current)))
	     (cond ((setq rest
			  (refine-rec nw-tar nw-cur (nth 3 selection) moves))
		    ; rest is solvable too
		    (return (cons (list current selection)
				  rest)))
		   (t			; Rest is not solvable
		    (of (list (list "Rest is not solvable")))))))))


;; for each group finds the moves that will be safe if that grous is
;; selected as the next stage, then sorts them by the number of those moves.

(defun sort-groups (groups current moves)
  (do ((grs groups (cdr grs)))
      ((null grs)
       (sort groups
	     #'(lambda (x y) (> (length (nth 3 x)) (length (nth 3 y))))))
      (nconc (car grs)
	     (moves-safe-after (caar grs) current moves))))


;;list of "moves" that will be safe after and potentially applicable to
;; the statement obtained by adding "target" to "current" statement.
;; This is the list of moves that can be used in the next stages,
;; if "target" is going to be the goal of the current stage.

(defun moves-safe-after (target current moves)
  (prog (new-statement safe-moves)
	(setq new-statement (add-stmt target current))
	(do ((moves moves (cdr moves)))
	    ((null moves))
	    (cond ((and (do ((stmt target (cdr stmt)))
			    ((null stmt) (return t))
			    (cond ((implies-a new-statement
					      (apply-move (caar stmt)
							  (cadar stmt)
							  (caddar stmt)
							  (car moves))))
				   (t (return))))
			(or (null (cadar moves)) ;no precondition
			    (pt-applicable (car moves) new-statement)))
		   (setq safe-moves (nconc safe-moves (list (car moves)))))))
	(remove-stmt target new-statement)
	(return (list safe-moves))))
;; returns
;;  ((target statement)
;;   (relevant moves)
;;   (irelevant moves)
;;   (moves safe after))








;;---------------------------------------------------------------------
;; MACRO-MAKER FUNCTIONS
;;---------------------------------------------------------------------

;; destructively adds the "macro" to MACROS if not there and returns "macro"
;; checks for duplicates for graph search.
;; MACROS are hashed using their sizes (# assignments)

(defun add-new-macro (macro)
  (declare (special MACROS))
  (let* ((size (length (cddr macro)))
	 (bucket (assoc size MACROS))
	 (new-bucket nil)
	 (same nil))
    (cond ((null (cddr macro)) nil)     ;null macro
	  ((null MACROS)		;create the first bucket
	   (setq MACROS (list (list size macro)))
	   macro)
	  ((null bucket)		;add a new bucket
	   (setq new-bucket (list size macro))
	   (cond ((< size (caar MACROS)) ;new bucket is the first
		  (setq MACROS (cons new-bucket MACROS)))
		 (t (do ((point MACROS (cdr point))) ;find the right place
			((null (cdr point)) ;add bucket to the end
			 (rplacd point (list new-bucket)))
			(cond ((< size (caadr point))
			       (rplacd point ; put right after point
				       (cons new-bucket (cdr point)))
			       (return))))))
	   macro)
	  ((setq same (member-move macro (cdr bucket)))
					; there is a macro with the same effect
	   (cond ((< (length (car macro)) (length (car same)))
		  (rplaca same (car macro))
		  nil)))
	  (t (nconc bucket (list macro)) ;add macro to the end of the bucket
	     macro))))


;; Sorts the assignments of "operator" in reverse order of VARIABLES.

(defun allign (operator)
  (declare (special VARIABLES))
  (do ((vars VARIABLES (cdr vars))
       (assignment)
       (sorted))
      ((null vars)
       (rplacd (cdr operator) sorted)
       (rplaca operator (list (car operator))))
      (cond ((setq assignment (assoc (car vars) (cddr operator)))
	     (setq sorted (cons assignment sorted))))))


;; returns a new macro equlivalent to applying "first" then "second" macros.
;; pcs is prepared under "current" statement.

(defun extend (first second current)
  (declare (special VARIABLES))
  (let ((name (append (car first) (car second)))
	(pcs (cond ((null (cadr second)) (cadr first))
		   (t (precond first second current)))))
    (cond ((eq pcs 'FALSE) nil)		; impossible
	  (t (do ((assignments) (frst-assig) (scnd-assig) (right-hand)
		  (vars VARIABLES (cdr vars)))
		 ((null vars)
		  (cond (pcs (setq assignments
				   (filter-assigs assignments pcs))))
		  (cons name (cons pcs assignments)))
		 (cond ((setq scnd-assig (assoc (car vars) 
						(cddr second)))
			(cond ((setq frst-assig 
				     (assoc (car (last scnd-assig))
					    (cddr first)))
			       (setq right-hand
				     (simplify 
				      (nconc (remove (car frst-assig)
						     (cdr scnd-assig))
					     (cdr frst-assig))
				      nil))
			       (cond ((eq (car vars) (car right-hand)))
				     (t (setq assignments
					      (cons (cons (car vars)
							  right-hand)
						    assignments)))))
			      (t (setq assignments
				       (cons scnd-assig assignments)))))
		       (t (cond ((setq frst-assig
				       (assoc (car vars) (cddr first)))
				 (setq assignments
				       (cons frst-assig assignments)))))))))))


;; filters out the unncessary assignments implied by the pcs

(defun filter-assigs (assignments pcs)
  (do ((assigs assignments (cdr assigs)))
      ((null assigs) assignments)
      (cond ((or (member (cons 'EQ (car assigs)) pcs 
			 :test #'equal)
		 (member (list 'EQ (cadar assigs) (caar assigs)) pcs 
			 :test #'equal))
	     (setq assignments (delete (car assigs) assignments 
				       :test #'equal))))))


;; (rel-moves * rel-moves) + (irr-moves * rel-moves).

(defun make-macros (problem)
  (nconc (multiply-moves (nth 2 problem) (nth 2 problem) (nth 1 problem))
	 (multiply-moves (nth 3 problem) (nth 2 problem) (nth 1 problem))))


;; returns t iff "move" is a member of "moves".

(defun member-move (move moves)
  (do ((moves moves (cdr moves)))
      ((null moves) nil)
      (cond ((eq-move move (car moves)) (return (car moves))))))


;; Returns the list of macros by multiplying a move from "M1"
;; by a move from "M2".

(defun multiply-moves (M1 M2 current)
  (do ((M1 M1 (cdr M1))
       (new-macros nil))
      ((null M1) new-macros)
      (do ((M2 M2 (cdr M2))
	   (macro))
	  ((null M2))
	  (setq macro (extend (car M1) (car M2) current))
	  (cond ((and (cddr macro)    ; not an identity macro
		      (add-new-macro macro))
		 (setq new-macros
		       (nconc new-macros (list macro))))))))


;; precondition statement of the macro which consists of applying "move1" first
;; then "move2".  FALSE if "move2" can not be applied after "move1".

(defun precond (move1 move2 p-list)
  (do ((current (add-stmt (cadr move1) (copy-tree p-list)))
       (new-pcs (cadr move1))
       (pcs2 (cadr move2) (cdr pcs2))
       (a-pcs2) (a-pcs2-m))
      ((null pcs2) (rm-tautologies new-pcs))
      (setq a-pcs2-m
	    (cons (caar pcs2)
		  (mapcar #'(lambda (e) (simplify e p-list))
			  (cdr (apply-move (caar pcs2) (cadar pcs2)
					   (caddar pcs2) move1)))))
      (setq a-pcs2 (cons (car a-pcs2-m) (mapcar 'car (cdr a-pcs2-m))))
      (cond ((member a-pcs2 new-pcs :test #'equal))	
					;a-pcs2 is already included in new-pcs
	    ((and (eq (car a-pcs2) 'EQ) ;equal symmetric
		  (member (list 'EQ (caddr a-pcs2) (cadr a-pcs2)) new-pcs 
			  :test #'equal)))
	    ((implies-a current (negate a-pcs2-m))
	     ; move2 cannot be applied after move1
	     (return 'FALSE))
	    (t	
	     (setq new-pcs (cons a-pcs2 new-pcs))
	     ; add a-pcs2 if not in current already
	     (cond ((member (caddr a-pcs2)
			    (cdr (assoc (car a-pcs2)
					(cdr (assoc (cadr a-pcs2) current))))))
		   (t (add-a-stmt a-pcs2 current)))))))


;; remove tautologies
(defun rm-tautologies (pcs)
  (do ((pcs pcs (cdr pcs))
       (taut-free))
      ((null pcs) taut-free)
      (cond ((and (eq (caar pcs) 'EQ)
		  (eq (cadar pcs) (caddar pcs))))
	    (t (setq taut-free (nconc taut-free (list (car pcs))))))))


;;----------------------------------------------------------------
;; DDKB (Domain Dependent Knowledge Base) FUNCTIONS
;;----------------------------------------------------------------

;; destructively adds "a-stmt" into the "p-list".

(defun add-a-stmt (a-stmt p-list)
  (rplacd (last (assoc (car a-stmt) 
		       (cdr (assoc (cadr a-stmt) p-list))))
	  (list (caddr a-stmt)))
  (cond ((or (eq (car a-stmt) 'EQ)
	     (eq (car a-stmt) 'NE))	; predicate is symmetric
	 (rplacd (last (assoc (car a-stmt) 
			      (cdr (assoc (caddr a-stmt) p-list))))
		 (list (cadr a-stmt)))))
  p-list)


;; Destructively adds "stmt" into "p-list".

(defun add-stmt (stmt p-list)
  (do ((stmt stmt (cdr stmt)))
      ((null stmt) p-list)
      (add-a-stmt (car stmt) p-list)))


;; Goes through the equivalents of "v1" in search for an a-stmt
;; (PRED V1-EQ VAR-2), where V1-EQ is an equivalent of "v1".
;; Returns T if found up to depth 2.

(defmacro pred-vars (pred var)
  `(cdr (assoc ,pred (cdr (assoc ,var p-list)))))

(defun go-thru-eqs (pred v1 v2 p-list)
  (or (member v2 (pred-vars pred v1))
      (do ((v2-eq (pred-vars 'EQ v2) (cdr v2-eq))
	   (v1-pr (pred-vars pred v1)))
	  ((null v2-eq))
	  (cond ((member (car v2-eq) v1-pr) (return t))))
      (do ((v1-eq (pred-vars 'EQ v1) (cdr v1-eq))
	   (v1-eq-pr)
	   (v2-eq (pred-vars 'EQ v2)))
	  ((null v1-eq))
	  (setq v1-eq-pr (pred-vars pred (car v1-eq)))
	  (cond ((member v2 v1-eq-pr)
		 (return t))
		((do ((v2-eq v2-eq (cdr v2-eq)))
		     ((null v2-eq))
		     (cond ((member (car v2-eq) v1-eq-pr) (return t))))
		 (return t))))))


;; true iff "p-list" statement implies "a-stmt".
;; "a-stmt" must be in the form of (PRED (EXP-1) (EXP-2)).

(defun implies-a (p-list a-stmt)
  (case (car a-stmt)
	 (EQ (test-EQ (cadr a-stmt) (caddr a-stmt) p-list))
	 (NE (test-NE (cadr a-stmt) (caddr a-stmt) p-list))
	 (GR (test-GR (cadr a-stmt) (caddr a-stmt) p-list))
	 (NG (test-NG (cadr a-stmt) (caddr a-stmt) p-list))))


;; t if "p-list" implies "stmt".

(defun implies (p-list stmt)
  (do ((stmt stmt (cdr stmt)))
      ((null stmt) t)
      (cond ((implies-a p-list (cons (caar stmt) 
				     (mapcar 'list (cdar stmt)))))
	    (t (return)))))


;;t iff "move" is potentially applicable to a state satisfying "p-list"

(defun pt-applicable (move p-list)
  (do ((pcs (cadr move) (cdr pcs))
       (added-pcs))
      ((null pcs) (remove-stmt added-pcs p-list) t)
      (cond ((implies-a p-list (cons (car (negate (car pcs)))
				     (mapcar 'list (cdar pcs))))
	     ; move cannot be applied to p-list
	     (remove-stmt added-pcs p-list)
	     (return))
	    (t		     ; add (car pcs) if not in p-list already
	     (cond ((member (caddar pcs)
			  (cdr (assoc (caar pcs)
				     (cdr (assoc (cadar pcs) p-list))))))
		   (t (add-a-stmt (car pcs) p-list)
		      (setq added-pcs (cons (car pcs) added-pcs))))))))


;; returns t if "move" is relevant to any "target" a-statement.That is,
;; There exists a "ti" that [current(s)+pcsm(s)+~ti(s) /-> ~ti(m(s))].

(defun relevant (move target current)
  (do ((target target (cdr target))
       (current (cond ((cadr move) (add-stmt (cadr move) 
					     (copy-tree current)))
		      (t current))))
      ((null target))			;return irrelevant
      (cond ((relevant-a move (car target) current)
	     (return t)))))                      ; relevant


;; returns t if "move" is relevant to "ti".
;; [current(s)+~ti(s) /-> ti(m(s))]

(defun relevant-a (move ti current)
  (prog (~ti ~ti-m irrel-p)
	(cond ((implies-a current (cons (car ti)
					(mapcar 'list (cdr ti))))
	       (return nil)))
	(setq ~ti (negate ti))
	(setq ~ti-m (apply-move (car ~ti) (cadr ~ti) (caddr ~ti) move))
	(setq irrel-p (implies-a (add-a-stmt ~ti current) ~ti-m))
	(setq current (remove-a-stmt ~ti current))
	(return (not irrel-p))))


;; destructively removes "a-stmt" from the "p-list".

(defun remove-a-stmt (a-stmt p-list)
  (delete (caddr a-stmt) (assoc (car a-stmt) (cdr (assoc (cadr a-stmt) p-list))))
  (cond ((or (eq (car a-stmt) 'EQ)
	     (eq (car a-stmt) 'NE))  ; predicate is symmetric
	 (delete (cadr a-stmt)
	       (assoc (car a-stmt) (cdr (assoc (caddr a-stmt) p-list))))))
    p-list)


;; destructively removes "stmt" from "p-list".

(defun remove-stmt (stmt p-list)
  (do ((stmt stmt (cdr stmt)))
      ((null stmt) p-list)
      (remove-a-stmt (car stmt) p-list)))


;; t iff "move" is safe over "p-list"
;; generates all the a-stmts in "p-list", and test if they remain after move.

(defun safe (move p-list)
  (do ((var-1 p-list (cdr var-1)))
      ((null var-1) t)
      (cond ((do ((pred (cdar var-1) (cdr pred)))
		 ((null pred) t)
		 (cond ((do ((var-2 (cdar pred) (cdr var-2)))
			    ((null var-2) t)
			    (cond ((implies-a p-list
					      (apply-move (caar pred)
							  (caar var-1)
							  (car  var-2)
							  move)))
				  (t (return)))))
		       (t (return)))))
	    (t (return)))))








;;---------------------------------------------------------------------
;; UTILITY FUNCTIONS
;;---------------------------------------------------------------------

;; applies "move" to the a-statement which is in the form of
;; (PRED VAR-1 VAR2).

(defun apply-move (pred var-1 var-2 move)
  (list pred
	(cond ((cdr (assoc var-1 (cddr move))))
	      (t (list var-1)))
	(cond ((cdr (assoc var-2 (cddr move))))
	      (t (list var-2)))))


;; t if "move-1" and "move-2" have the same effect on the "statement".

(defun eq-effect-moves (move-1 move-2 statement)
  (do ((assig-1 (cddr move-1))
       (assig-2 (cddr move-2))
       (eff-vars (get-vars statement) (cdr eff-vars)))
      ((null eff-vars) (return t)) ;move-1 and move-2 have equal effect
      (cond ((equal (cdr (assoc (car eff-vars) assig-1))
		    (cdr (assoc (car eff-vars) assig-2))))
	    (t ;different
	     (return nil)))))

  
;; list of variables mentioned in the target statement.

(defun get-vars (statement)
  (do ((stmt statement (cdr stmt))
       (vars))
      ((null stmt) vars)
      (cond ((member (cadar stmt) vars))
	    (t (setq vars (cons (cadar stmt) vars))))
      (cond ((member (caddar stmt) vars))
	    (t (setq vars (cons (caddar stmt) vars))))))


;; t if "move-1" and "move-2" are equal.

(defun eq-move (move-1 move-2)
  (and (equal (cddr move-1) (cddr move-2))      ;same assignments
       (eq-set (cadr move-1) (cadr move-2))))	;same pcs


;; t if "set-1" and "set-2" are equal

(defun eq-set (set-1 set-2)
  (and (subsetp set-1 set-2 :test #'equal)
       (subsetp set-2 set-1 :test #'equal)))


;; makes binary predicates from "predicate".
(defun expand-pred (predicate)
  (cond ((eq (car predicate) 'FOR-ALL)
	 (for-all (cadr predicate) (caddr predicate) (cadddr predicate)))
	((eq (car predicate) 'FOR-ALL-S)
	 (for-all-S (cadr predicate) (caddr predicate)))
	((eq (car predicate) 'FOR-ALL-S-S)
	 (for-all-S-S (cadr predicate) (caddr predicate) (cadddr predicate)))
	(t (list predicate))))


;; For all si in S1 (for all sj in S2, (R si sj))

(defun for-all-S-S (R S1 S2)
  (mapcan #'(lambda (si)
	      (for-all R si S2))
	  S1))


;; For all si in "S" (for all sj>i in S, (R si sj)).

(defun for-all-S (R S)
  (do ((S S (cdr S))
       (result))
      ((null (cdr S)) result)
      (setq result
	    (nconc result (for-all R (car S) (cdr S))))))


;; For all sj in "S", (R si sj).

(defun for-all (R si S)
  (mapcar #'(lambda (sj)
	      (list R si sj))
	  S))


;; negates the "a-stmt".

(defun negate (a-stmt)
  (case (car a-stmt)
	(EQ (cons 'NE (cdr a-stmt)))
	(NE (cons 'EQ (cdr a-stmt)))
	(GR (cons 'NG (cdr a-stmt)))
	(NG (cons 'GR (cdr a-stmt)))))


;; prints the text in a file called "output".

(defun of (text)
  (let ((port (open "output" 
		    :direction :output
		    :if-exists :append
		    :if-does-not-exist :create)))
    (cond ((null text) (terpri) (terpri port))
	  (t (do ((text text (cdr text)))
		 ((null text))
		 (princ (car text)) (terpri)
		 (princ (car text) port) (terpri port))))
    (close port)))


;; prints each element of the list IN on a sperate line of standard output

(defun pr (in)
  (do ((in in (cdr in)))
      ((null (cdr in)) (terpri) (car in))
      (print (car in))
      (terpri)))