;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: jqueens
;;;;    System: JTMS
;;;;    Author: Kenneth D. Forbus, Northwestern University,
;;;;            Johan de Kleer, and Xerox Corporation
;;;;   Created: January 23, 2000 10:32:09
;;;;   Purpose: Example of dependency-directed search using JTRE.
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Sunday, January 23, 2000 at 10:39:56 by ferguson
;;;; ---------------------------------------------------------------------------

;;; Copyright (c) 1986--1992 Kenneth D. Forbus, Northwestern University,
;;; Johan de Kleer and Xerox Corporation.
;;; All rights reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(in-package :cl-user)

;;; Statistics
(defvar *n-assumptions* 0)
(defvar *placements* nil  "Set of valid placements.")


(defun test-queens (from to)
  "Test the N-queens problem solver for given range of board sizes."
  (do ((n from (1+ n)))
      ((> n to))
      (gc)
      (time (n-queens n))
      (format t "~% For n=~D, ~D solutions, ~D assumptions."
	     n (length *placements*) *n-assumptions*)))

(defun n-queens (n &optional (debugging? nil))
  "Solve the N-queens puzzle for a given board size.  Returns number of valid
   placements, and sets *placements* to the valid placement sets."
  (setup-queens-puzzle n debugging?)
  (solve-queens-puzzle (make-queens-choice-sets n))
  (length *placements*))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Setup and search

(defun setup-queens-puzzle (n &optional (debugging? nil))
  (in-jtre (create-jtre (format nil "~D-Queens JTRE" n) 
			:debugging debugging?))
  (setq *placements* nil
	*n-assumptions* 0)
  (bps-load-file *jtre-path* *jqueen-rule-file* :action :source-if-newer))

(defun make-queens-choice-sets (n)
  "Create a set of choice sets for placement of N queens on
   an NxN chessboard."
  (do ((column 1 (1+ column))
       (column-queens nil nil)
       (choice-sets nil))
      ((> column n) (nreverse choice-sets))
    (dotimes (row n)
     (push `(queen ,column ,(1+ row)) column-queens))
    (push (nreverse column-queens) choice-sets)))

(defun solve-queens-puzzle (choice-sets)
  "Test each of the choice sets, marking bad solutions as nogoods."
  (cond ((null choice-sets) (gather-queens-solution))
	(t (dolist (choice (car choice-sets))
	    (unless (in? `(not ,choice) *jtre*)
	     ;respect nogood information
     (multiple-value-bind (nogood? asns)
      (try-in-context choice
       `(solve-queens-puzzle ',(cdr choice-sets))
       *jtre*)
      (incf *n-assumptions*)
      (when nogood?
	    ;;This assumption lost, so justify the negation
	    ;; based on the other relevant assumptions.
	    (assert! `(not ,choice)
		     `(Nogood ,@ 
			      (remove choice asns))))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; JTMS approximation to try-in-context

(defun try-in-context (asn thunk jtre &aux try-marker result)
  (setq try-marker (cons 'TRY asn))
  (with-contradiction-handler (jtre-jtms jtre)
        #'(lambda (jtms contras)
	    (try-contradiction-handler
	     contras jtms asn try-marker jtre))
        (unwind-protect
	  (progn (unless (in? asn jtre)
		   (setq result (catch 'try-contradiction-found
				  (assume! asn try-marker jtre)))
		   (when (and (listp result) (eq (car result) :asns))
		     (return-from try-in-context
				  (values t (mapcar #'view-node
						    (cdr result)))))
		   (setq result (catch 'try-contradiction-found
				  (run-rules jtre)))
		   (when (and (listp result)  (eq (car result) :asns))
		     (return-from try-in-context
				  (values t (mapcar #'view-node
						    (cdr result)))))
		   (eval thunk) ;; use the thunk
		   (progn (retract! asn try-marker t)
			  (return-from try-in-context
				       (values nil nil))))))))

(defun try-contradiction-handler (contras jtms asn marker *jtre* &aux node)
  "When a contradiction occurs, this funciton is called with a list of
   contradiction nodes.  Function retracts the first assumption it
   finds among the set of antecedents, and throws to TRY-CONTRADICTION-FOUND
   tag."
  (unless (eq jtms (jtre-jtms *jtre*))
    (error "~%High Contradiction Weirdness: ~A not jtms for ~A!"
	   jtms *jtre*))
  (unless contras (return-from try-contradiction-handler nil))
  (unless asn (return-from try-contradiction-handler nil))
  (setq node (get-tms-node asn))
  (dolist (cnode contras)
    (let ((asns (assumptions-of-node cnode)))
      (when (member node asns)
	(retract! asn marker)
	(throw 'try-contradiction-found (cons :asns asns))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Other helpers

(defun queens-okay? (x1 y1 x2 y2)
  "True if the two queens cannot capture one another."
  (not (or (= y1 y2) (= (abs (- x1 x2)) (abs (- y1 y2))))))

(defun gather-queens-solution ()
  (push (remove-if #'(lambda (q) (out? q *jtre*))
		   (fetch `(Queen ?c ?r) *jtre*))
	*placements*))

(defun show-queens-solution (solution &aux n)
  "Show an N-queens solution in a spatial format."
  (setq n (length solution))
  (dotimes (i n)
    (terpri)
    (dotimes (j n)
      (format t "~A"
	      (if (member `(queen ,i ,j) solution
			  :test #'equal) "Q" "-")))))