;;; -*- Mode: Lisp; Syntax: Common-lisp; -*-
;;;; File name: dds.lsp
;;;; Dependency-directed search facility
;;;;  Modified: Wednesday, January 26, 2005 at 09:45:12 by Kenneth Forbus

;;; Copyright (c) 1993, Kenneth D. Forbus, Northwestern University,
;;; and Johan de Kleer, the 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)

(defvar *debug-dds* nil)

(defmacro debug-dds (str &rest args)
  `(if *debug-dds* (format t ,str ,@ args)))

(defun dd-search (choice-sets end &aux answer marker choices)
  (when (null choice-sets)
    (debug-dds "~%    DDS: Found solution.")
    (eval end)
    (return-from dd-search nil))
  (setq marker (list 'DDS (car choice-sets)))
  (setq choices (car choice-sets))
  (dolist (choice choices)
    (debug-dds "~%    DDS: considering ~A..." choice)
    (cond ((false? choice) ;skip if known loser
	   (debug-dds "~%    DDS: ~A already known nogood." choice))
	  ((true? choice) ;continue if known
	   (debug-dds "~%    DDS: ~A true by implication." choice)
	   (dd-search (cdr choice-sets) end)
	   (return nil))
          (t (debug-dds "~%    DDS: Assuming ~A." choice)
             (with-contradiction-handler (ltre-ltms *ltre*)
               #'(lambda (clauses ltms &aux asns)
                   (declare (ignore ltms))
                   (debug-dds "~%    DDS: Entering handler for ~A with ~A~A."
                    choice clauses
                    (mapcar #'(lambda (c) (violated-clause? c))
                       clauses))
                   (dolist (cl clauses)
                      (setq asns (assumptions-of-clause cl))
                      (debug-dds "~%    DDS: Assumptions are: ~A"
                        asns)
                      (dolist (asn asns)
                         (when (or (equal choice (view-node asn))
                                   (and (listp choice) (eq (car choice) :not)
                                        (equal (cadr choice) (view-node asn))))
                            (throw marker
                               (cons :losers ;; Assign labels before any retraction
                                  ;; Failure to do so can result in incorrect nogoods.
                                  (mapcar #'signed-view-node
                                     (delete asn asns))))))))
              (setq answer (catch marker
                              (assuming (list choice) *ltre*
                               (run-rules *ltre*)
                               (dd-search (cdr choice-sets) end))))
              (when (and (listp answer)
                         (eq (car answer) :losers))
                 (debug-dds "~%    DDS: ~A inconsistent with ~A."
                  choice (cdr answer))
                 (assert! `(:not (:and ,choice
                                  ,@ (cdr answer)))
                  :dd-search-NOGOOD)))))))

;;;; A familiar example

(defun test-dd-search (&optional (debugging? t))
  (in-ltre (create-ltre "DDS Test" :debugging debugging?))
  (eval '(rule ((:true A) (:true C))
	       (rassert! (:not (:and A C)) :domain-nogood)))
  (eval '(rule ((:true B) (:true E))
	       (rassert! (:not (:and B E)) :domain-nogood)))
  (dd-search '((A B) (C D) (E F)) 
	     '(show-dd-test-solution)))
	    
(defun show-dd-test-solution (&aux result)
  (dolist (var '(F E D C B A))
    (when (true? var *ltre*) (push var result)))
  (format t "~% consistent solution: (~A)." result))