" (c) 1992,1993,1994 Copyright (c) University of Washington
  Written by Tony Barrett.

  All rights reserved. Use of this software is permitted for non-commercial
  research purposes, and it may be copied only for that use.  All copies must
  include this copyright message.  This software is made available AS IS, and
  neither the authors nor the University of Washington make any warranty about
  the software or its performance.

  When you first acquire this software please send mail to
  bug-ucpop@cs.washington.edu; the same address should be used for problems."

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; The following code is used to implement variable codesignation constraints.
;;; This code was created after looking at Steve Hanks's use of varsets.
;;; 
;;;

(in-package "VARIABLE")

(export '(unify unify-args bind-variable instantiate-term
	  add-bind new-bindings variable? uniquify-var
	  test-equivalence
	  *unify-count* *compute-rank-unifies* 
	  *computing-rank* *add-bind-count*))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Outline of this file
;;;
;;; 1. Structures used for implementing constraints
;;; 2. A handy interface function to unify two lists using constraint sets
;;; 3. CONSTRAINT SETS (CS)
;;; 4. VARSETS:  Each VARSET represents a set of codesignating variables.
;;; 5. VARIABLES  -- 
;;; 6. Print functions

;;;***************************************************************************
;;; 1. Structures used for implementing constraints

(defstruct (varset (:print-function print-varset))
  const         ;; the unique constant that codesignates with this varset.
  cd-set        ;; the set of variables (and constant) that codesignate
  ncd-set)	;; Vars & consts that must not codesignate with this set

(defstruct (var (:print-function print-variable))
  name					; The variable's name
  num)
  
(defvar *unify-count* 0)		; # of variable unifications made
(defvar *compute-rank-unifies* nil)	; # of unifications made in rank fn
(defvar *computing-rank* nil)		; flag: are we computing a rank?
(defvar *add-bind-count* 0)		; # of times new bindings were added
(defvar *free-vsets* nil)		; free varsets generated by unify
(defvar *context-alst* nil)		; Association list of known variables

;;;***************************************************************************
;;; 2. A handy interface function to unify two lists using constraint sets

;;;;;;;;;;;;;;;;;;;;;;;;                                                  
;;; Test whether two conditions can be unified consistent with plan bindings
;;; Returns a list of the list of bindings needed to unify, i.e. has an extra
;;; set of parentheses.  Returns nil if they cannot be unified.  Returns (nil)
;;; if they unify with no additional bindings.
(defun UNIFY (cond1 cond2 bindings)
  ;; fix Jscott's bug
  (when (and (eq (car cond1) :not) (eq (car cond2) :not))
    (setf cond1 (cadr cond1)
	  cond2 (cadr cond2)))
  (when (eq (car cond1) (car cond2))
    (unify-args (cdr cond1) (cdr cond2) bindings)))

(defun UNIFY-ARGS (args1 args2 bindings)
  (let ((result nil)
	(a1 nil)
	(a2 nil)
	(cs (list (car bindings))))
    (do ((b1 args1 (cdr b1))
	 (b2 args2 (cdr b2)))
	((null b1) (free-vsets (car cs) (car bindings)
			       (when (null b2) (list result))))
      (incf *unify-count*)
      (if *computing-rank* (incf *compute-rank-unifies*))
      (setf a1 (get-vset (car b1) cs))
      (setf a2 (get-vset (car b2) cs))
      (when (not (eq a1 a2))
	(push (cons (if (varset-const a1) (varset-const a1) (car b1))
		    (if (varset-const a2) (varset-const a2) (car b2)))
	      result)
	(let ((c (combine-varset a1 a2)))
	  (if c (push c (car cs))
	    (return-from unify-args
	      (free-vsets (car cs) (car bindings) nil))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Replace variable with associated constant from plan-bindings
;;; Leave as a variable if not bound to a constant
(defun BIND-VARIABLE (var bindings)
  (cond ((null var) nil)
	((listp var) (mapcar #'(lambda (x) (bind-variable x bindings))
			     var))
	(t (sym-value var bindings))))

(defun NEW-BINDINGS ()
  (new-cs))

(defun TEST-EQUIVALENCE (a b bindings)
  (cond ((eq a b) :true)
	(t (let* ((cs (list (car bindings)))
		  (a1 (get-vset a cs))
		  (b1 (get-vset b cs)))
	     (cond ((eq a1 b1) :true)
		   ((combine-varset a1 b1) :possible)
		   (t :impossible))))))

;;;;;;;;;;;;;;;;;;;;;;;;
;;; Changes variable symbols in the list into variable structures in
;;; the context NUM.
(defun INSTANTIATE-TERM (term num &optional (alst nil))
  (cond ((consp term) 
	 (mapcar #'(lambda (x) (instantiate-term x num alst))
		 term))
	((variable? term)
	 (let ((u (assoc term alst)))
	   (if u (cdr u) (make-variable term num))))
	(t term)))

;;;;;;;;;;;;;;;;;;;;;;;;                                                  
;;;  Add new entries to bindings
;;;  1st input is list of pairs of 2 terms, each pair possibly preceded by :not
(defun ADD-BIND (new-bind bindings)
  (when bindings
    (setf bindings (copy-cs bindings))
    (dolist (pair new-bind bindings)	; 
      (incf *add-bind-count*)
      (if (not (if (eql :not (car pair))
		   (constrain-neq (cadr pair) (cddr pair) bindings)
		 (constrain-eq (car pair) (cdr pair) bindings)))
	  (return-from add-bind nil))))
  bindings)

;;;***************************************************************************
;;; 3. CONSTRAINT SETS (CS) --
;;;   A constraint set is a list of varsets
;;;

(defun new-cs () 
  "Create a new constraint set."
  (list nil))

(defun copy-cs (cs) 
  (list (car cs)))

(defun constrain-eq (sym1 sym2 cs)
  "Ensure that two symbols codesignate in a constraint set.
   Returns nil if symbols cannot codesignate."
  (let* ((v1 (get-vset sym1 cs))
	 (v2 (get-vset sym2 cs))
	 (vs (combine-varset v1 v2)))
    (when vs
      (if (not (eq v1 v2)) (push vs (car cs)))
      t)))

(defun constrain-neq (sym1 sym2 cs)
  "Make sure that two symbols never codesignate in a constraint set.
   Returns nil if symbols already codesignate."
  (let* ((r1 (get-vset sym1 cs))
	 (v1 (restrict-varset r1 sym2))
	 (r2 (get-vset sym2 cs))
	 (v2 (restrict-varset r2 sym1)))
    (when (and v1 v2)
      (push v1 (car cs))
      (push v2 (car cs))
      t)))

(defun codesignates (sym1 sym2 cs)
  "Test to see if two symbols explicitely codesignate."
  (member sym2 (varset-cd-set (get-vset sym1 cs))))

(defun sym-value (sym cs)
  "Get the value of a symbol.  It might be a constant or variable."
  (if (variable? sym)
      (let ((v (get-vset sym cs)))
	(if (varset-const v) (varset-const v) 
	  (first (varset-cd-set v))))
    sym))

(defun get-vset (sym cs)
  "Get the varset associated with a symbol.  Might have to create it."
  (if (variable? sym)
      (dolist (l (car cs))
	(dolist (v (varset-cd-set l))
	  (when (eq v sym) (return-from get-vset l))))
    (dolist (l (car cs))
      (when (eql (varset-const l) sym) 
	(return-from get-vset l))))
  (car (push (make-empty-varset sym) (car cs))))

;;;***************************************************************************
;;; 4. VARSETS:  Each VARSET represents a set of codesignating variables.
;;; Store for each 
;;;    (1) the constant (if any) they codesignate with, and 
;;;    (2) a set of codesignating variables and possibly a constant
;;;    (3) a set of constants and variables they CANNOT codesignate with.
;;;
;;; Some thoughts on VARSETs...
;;;   - The codesignation sets form equivalence classes.  This means that
;;;     the cd sets in the varsets are disjoint.
;;;   - Constants have varsets too!  This means that the only place that we
;;;     have to explicitely reason about a constant is to make sure that no
;;;     two unique constants codesignate.
;;;   - Since the cd sets in each varset contain all codesignating symbols,
;;;     there is no need to make sure that all symbols that must not 
;;;     codesignate are in the ncd lists.  Puting only one element of a 
;;;     codesignating varset in the ncd is enough to ensure that the
;;;     noncodesignating varsets can never get combined.
;;;

(defmacro var-union (a b) ; &aux ret
  `(union ,a ,b :test #'eql))

(defmacro var-intersect? (a b)
  `(intersection ,a ,b :test #'eql))

(defun make-empty-varset (symb)
  "Make a new varset for SYMB (if it has never been seen before).
   Constants appear in varsets too!"
  (new-varset :cd-set (list symb)
	      :const (if (variable? symb) nil symb)
	      :ncd-set nil))

(defun combine-varset (a b)
  "Combine two varsets.  (called for each codesignation constraint)"
  (if (eq a b) a
      (when (or (null (varset-const a))
		(null (varset-const b)))
	(let ((cd-set  (append (varset-cd-set a) (varset-cd-set b)))
	      (ncd-set (var-union (varset-ncd-set a) (varset-ncd-set b)))
	      (const   (if (varset-const a) (varset-const a)
			   (varset-const b))))
	  (when (and (not (member const ncd-set :test #'eql))
		     (not (var-intersect? cd-set ncd-set)))
	    (new-varset :const const
			:cd-set cd-set
			:ncd-set ncd-set))))))

(defun restrict-varset (vset restricter)
  "Make sure that VSET never codesignats with a varset containing RESTRICTER."
  (when (not (member restricter (varset-cd-set vset) :test #'eql))
    (new-varset :const (varset-const vset)
		:cd-set (varset-cd-set vset)
		:ncd-set (var-union (list restricter) 
				     (varset-ncd-set vset)))))

(defun new-varset (&key const cd-set ncd-set)
  (if *free-vsets*
      (let ((v (pop *free-vsets*)))
	(setf (varset-const v) const
	      (varset-cd-set v) cd-set
	      (varset-ncd-set v) ncd-set)
	v)
    (make-varset :const const :cd-set cd-set :ncd-set ncd-set)))

(defun free-vsets (v1 v2 ret-val &aux a)
  (do ()
      ((eq v1 v2) ret-val)
    (setf a v1)
    (setf v1 (cdr v1))
    (setf (cdr a) *free-vsets*)
    (setf *free-vsets* a)))
	    
;;;**************************************************************
;;; 5. VARIABLES  -- This code was written by Steve Hanks 
;;;                            and modified by J Scott Penberthy
;;;

(defvar *variable-cache* (make-hash-table :test #'equal))

(defun variable? (thing)
  (or (and (symbolp thing)
	   (char= #\? (elt (symbol-name thing) 0)))
      (var-p thing)))

(defun uniquify-var (var)
  (if (symbolp var) (make-var :name var :num nil)
    (make-var :name (var-name var) :num (var-num var))))

(defun make-variable (var num)
  (let ((vs (gethash var *variable-cache*)))
    (dolist (v vs (car (push (make-var :name var :num num) 
			     (gethash var *variable-cache*))))
      (when (eql num (var-num v))
	(return v)))))

;;;***************************************************************************
;;; 6. Print functions
;;;

(defun print-varset (self stream depth)
  (declare (ignore depth))
  (format stream "<VARSET {~a} = ~a not~a>" 
          (varset-cd-set self) 
          (varset-const self) 
          (varset-ncd-set self)))

(defun print-variable (self stream depth)
  (declare (ignore depth))
  (format stream "~a~a" (var-name self)(var-num self)))

