;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: clause-optimizer.lsp
;;;;    System: FIRE
;;;;    Author: Ken Forbus
;;;;   Created: September 29, 2003 09:50:33
;;;;   Purpose: Optimizing clauses for backchaining
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Wednesday, June 2, 2004 at 14:31:54 by hinrichs
;;;; ---------------------------------------------------------------------------

(in-package :fire)

;;;;; Clause term optimizer
;;
;; A complication in backchaining is that many predicates are handled
;; by reasoning sources.  Reasoning sources are often procedural, so
;; there are only certain directions of inference that make sense.
;; There are two signatures, a query signature and a result signature.
;; For the query signature:
;; For fixed-arity predicates:
;; Each argument entry consists of a constraint,
;; where <constraint> = :VARIABLE | :KNOWN 
;;                        | (:ISA <type>) | (:TEST <procedure>) | :ANYTHING
;; The meanings of the <constraint> entries are
;;  :VARIABLE the query has a pattern in that position.
;;  :KNOWN the query has something that isn't a variable in that position.
;;  (Issue: What about NATs?  Should :VARIABLE = non-ground, :KNOWN = ground?)
;;  (:ISA <type>) is like :KNOWN, but the argument must be a member of the 
;;    collection <type>.
;;  (:TEST <procedure>) is like :KNOWN, but the argument must satisfy the Lisp
;;    procedure <procedure>.  (Good for filtering out non-numerical args, for instance.)
;;  :ANYTHING means no constraint on that argument.
;;
;; The result signature indicates what can be treated as inputs versus outputs
;; (There is some redundancy here with the query signature, of course.)
;; The three values are 
;;   :input-only means this has to be specified as an input.
;;   :produces means this is an output from the underlyng procedural attachment.
;;   :can-produce means it can either be an input or an output.
;;
;; For n-ary predicates, things are a bit complex because we would like to advertise
;; correctly when a source can or cannot solve a problem.  For instance, a numerical 
;; constraint solver source might want to say
;; :ALL means the constraint must be satisfied for all arguments.
;; :SOME means the constraint must be satisfied for at least one argument.
;; <integer> means exactly that number of arguments must satisfy the constraint.
;; :REST means that, with the exception of arguments that satisfy some other constraint,
;;  every remaining argument must satisfy the given constraint. If there are no other
;;  constraints this equivalent to :ALL.  It is an error to have more than one :REST
;;  constraint in a query signature.
;; (See sources.lsp for code that supports this)
;;
;; While reasoning sources are essential to FIRE's efficient operation,
;; they have a regrettable negative interaction with backchaining.  In
;; backchaining it is assumed that, given a term one enters a clause with,
;; one can then proceed to attempt solving the other clauses in the term
;; in any order.  Such is not the case with predicates handled by reasoning
;; sources, since the constraints outlined above have to be satisfied. 
;;
;; This has a significant implication for the overall structure of FIRE:
;; It means that chainers have to be defined with respect to a set of
;; sources -- they are no longer a function only of the KB.  This means that
;; we will need to store some kind of information about sources that will enable
;; a reasoner to tell whether a chainer would be appropriate for it.

;; Exclusive Handling Heuristic: We assume that if a predicate is handled by
;; a reasoning source, it cannot be backchained on.  This is a reasonable
;; heuristic because most predicates are not overloaded, and one can always
;; define a second predicate that can be backchained on to work around cases
;; where one has both axioms and sources to use for the same information.
;; The advantage of this heuristic is that it will prevent the backchainer
;; from subgoaling on such predicates, and greatly limits the orders of 
;; querying that make sense.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Analyzing predicate chaining properties
;;
;; Given the Exclusive Handling Heuristic, we lump the predicates found in terms
;; into one of three categories:
;; OUTSOURCED: There exists some source which can supply it, for some combination of
;;    input bindings.
;; FLOATING: The predicate itself is currently a variable.
;; CHAINED: The predicate is neither outsourced nor floating.  
;;
;; Outsourced predicates cannot be an entry point for backchaining.
;; Can floating predicates?  We'll assume not.  Heuristically, anything that
;; looks at all predicates of arity N is almost certainly going to be a very
;; bad idea.
;;

(defmethod outsourced-predicate? ((pred t)) nil)

(defmethod outsourced-predicate? ((pred symbol))
  (or (handled-via-ask? pred)
      (predicate-has-source? pred *reasoner*)))

;; ****** isa is an interesting case.  Many times it is handled by
;; ****** ask, but not always.  

(defun handled-via-ask? (pred)
  (or (eq pred 'data::genls) ;; Structural procedures should suffice.
      (eq pred 'data::equals)
      (eq pred 'data::different)
      (eq pred 'data::alphalessp)
      (metaknowledge-predicate? pred)
      (structural-predicate? pred)
      (eq pred 'data::evaluate)))

(defun floating-predicate? (pred &optional (var-list nil))
  (or (and (variable? pred) (not (member pred var-list)))
      (and (not (ground-formula? pred))
           (not (kappa-form? pred)))))

(defun chained-predicate? (pred)
  (not (or (handled-via-ask? pred)
           (floating-predicate? pred))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Deriving workable order of solutions

(defun derive-feasible-solution-orderings-for-terms (terms)
  (do ((term (car terms) (car other-terms))
       (other-terms (cdr terms) (cdr other-terms))
       (previous nil (cons term previous))
       (term-table nil))
      ((null term) term-table)
    (push (cons term 
                (derive-feasible-solution-orderings-for-term 
                 term (append previous other-terms)))
          term-table)))

(defun derive-feasible-solution-orderings-for-term (term other-terms)
  ;; Given a term in a clause, for each possible input signature, 
  ;; we derive a reasonable ordering.  The results are used in a
  ;; table stored with the clause.  
  (let ((ordering-table nil))
    (dolist (input-signature (generate-input-signatures (term-form term))
                             ordering-table)
      (let ((ordering (generate-query-order-from-input-signature
                       input-signature other-terms)))
        (unless (eq ordering :fail)
          (let ((entry (assoc ordering ordering-table :test 'equal)))
            (unless entry
              (setq entry (cons ordering nil))
              (push entry ordering-table))
            (push input-signature (cdr entry))))))))

(defun generate-input-signatures (term)
  (mapcar #'(lambda (l) (sort (copy-list l) 'ltre::alphalessp))
    (enumerate-binary-inclusion-combinations
     (formula-variables term))))

(defun enumerate-binary-inclusion-combinations (items)
  ;; Assume that items is never very long
  (cond ((null items) nil)
        ((null (cdr items)) (list (list (car items)) nil))
        (t (let ((sub-solutions (enumerate-binary-inclusion-combinations
                                 (cdr items))))
             (append (mapcar #'(lambda (other) (cons (car items) other))
                       sub-solutions)
                     sub-solutions)))))

(defun generate-query-order-from-input-signature (inputs other-terms)
  (multiple-value-bind (outsourced floating chained)
      (analyze-term-predicate-types other-terms inputs)
    (generate-query-order inputs 
                           (mapcar #'(lambda (p)
                                       (generate-term-state p inputs))
                             outsourced)
                           (mapcar #'(lambda (p)
                                       (generate-term-state p inputs))
                             floating)
                           (mapcar #'(lambda (p)
                                       (generate-term-state p inputs))
                             chained))))

(defun analyze-term-predicate-types (other-terms inputs)
  (let ((outsourced nil) (floating nil) (chained nil))
    (dolist (term other-terms (values outsourced floating chained))
      (let ((form (term-form term))
            (predicate nil))
        (cond ((quantified-term? form)  ;; (TRH)
               (push term chained))
              ((listp form)
               (setq predicate (car form))
               (cond ((outsourced-predicate? predicate)
                      (push term outsourced))
                     ((floating-predicate? predicate inputs)
                      (push term floating))
                     ((chained-predicate? predicate)
                      (push term chained))
                     (t (error "Predicate misclassification for ~A in ~A: ~A."
                          predicate form other-terms))))
              (t
               (error "Literal in term must be an expression: ~A, in ~A."
                 form other-terms)))))))

;;; Some heuristics:
;;;
;;; Outsourced predicates are preferred, since they tend to have something
;;; specialized that implements them.
;;;
;;; floating predicates will be done last, since we have nearly zero information
;;; about them at analysis time.
;;;
;;; We will generate at most one order.  If there is no order that is legal at
;;; analysis time, that combination will be punted immediately at run-time.

(defun generate-query-order (inputs outsourced-ps floating-ps chained-ps)
  (when (or outsourced-ps floating-ps chained-ps)
    (let ((feasible-orderings
           (generate-feasible-query-orderings inputs outsourced-ps
                                              floating-ps chained-ps)))
      (cond ((null feasible-orderings) :fail)
            ;; Pick first -- could sort, but not clear yet what heuristics
            ;; are best.
            (t (car feasible-orderings))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;

(defun generate-feasible-query-orderings (inputs outsourced-ps floating-ps chained-ps)
  ;; Here we bit the bullet and generate them all.  In part to be sure we don't miss
  ;; any, but also to see what the space looks like
  (let ((candidates (append outsourced-ps chained-ps floating-ps))
        (feasible-orderings nil))
    (dolist (candidate candidates feasible-orderings)
      (when (term-is-feasible? candidate)
        (let ((new-inputs (append inputs
                                  (vars-bound-by-match candidate))))
          ;; new-inputs models the state of what is known after a presumed
          ;; successful solution of the candidate term.
        (setq feasible-orderings
              (append feasible-orderings
                     (generate-feasible-query-orderings-for
                      new-inputs 
                      (list (fourth candidate))
                      (update-term-states-via-inputs
                       new-inputs (remove candidate candidates :test 'equal))))))))))

(defun generate-feasible-query-orderings-for (inputs so-far rest)
  (cond ((null rest) (list (reverse so-far)))
        (t (let ((solutions nil))
             (dolist (candidate rest solutions)
               (if (term-is-feasible? candidate)
                 (let ((new-inputs
                        (append inputs 
                                (vars-bound-by-match candidate))))
                   (setq solutions (append solutions
                                          (generate-feasible-query-orderings-for
                                           new-inputs (cons (fourth candidate) so-far)
                                           (update-term-states-via-inputs
                                            new-inputs
                                            (remove candidate rest
                                                    :test 'equal))))))))))))        

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Helpers for generate-query-order and its helpers

(defun update-term-states-via-inputs (new-inputs term-states)
  (mapcar #'(lambda (ts) (update-term-state new-inputs ts))
    term-states))

(defun find-best-next-term-candidate (term-states)
  (let ((feasible nil)
        (not-yet nil))
    (dolist (ts term-states)
      (if (term-is-feasible? ts) (push ts feasible)
        (push ts not-yet)))
    (cond ((null feasible) (values :fail term-states))
          ((= (length feasible) 1) ;; Go for it
           (values (car feasible) not-yet))
          (t (multiple-value-bind (best rest)
                 (pick-best-next-term-candidates feasible)
               (values best (append rest not-yet)))))))

(defun pick-best-next-term-candidates (feasible-ts)
  ;; Heuristic: Prefer the most bound variables.
  ;; If those are equal, prefer the most variables newly bound.
  (let ((by-boundedness
         (mapcar 'car 
           (sort (mapcar #'(lambda (ts)
                             (list ts 
                                   (number-of-vars-already-bound ts)
                                   (number-of-vars-bound-by-match ts)))
                   feasible-ts) #'(lambda (x y)
                                    (if (> (cadr x) (cadr y)) t
                                      (if (< (cadr x) (cadr y)) nil
                                        (> (third x) (third y)))))))))
    (values (car by-boundedness) (cdr by-boundedness))))
                                   

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Analyzing what is known in a pattern
;;; For this static analysis we are assuming that certain variables
;;; are known, and figuring out what to do as a consequence.
;;; This means we have to know, for each term, what its operator and argument
;;; depend upon in terms of pattern variable bindings.  
;;;
;;; The idea of a "term-state" captures the intermediate state of terms when
;;; doing the static analysis.
         
(defun generate-term-state (pattern inputs)
    (let ((pattern-entry (generate-term-entry pattern)))
      (cons (derive-pattern-known-state inputs pattern-entry)
            pattern-entry)))

(defun term-state-term (ts) (car (last ts)))

(defun generate-term-entry (pattern)
  ;; This is really a term, so pattern = (<real pattern> . <sign>)
  ;; pattern-entry = (<dependencies> <ask signatures> <term form>)
  (list (generate-pattern-variable-dependencies (car pattern))
        (pattern-ask-signatures (car pattern) *reasoner*)
        pattern))

(defun pattern-ask-signatures (pattern reasoner)
  (unless (quantified-term? pattern)  ; (TRH)
    (let ((predicate-signatures (predicate-ask-signatures (car pattern) reasoner)))
      (cond ((eq predicate-signatures :need-arguments)
             (argument-based-predicate-signature (car pattern) (cdr pattern)
                                                 reasoner))
            (t predicate-signatures)))))

(defmethod argument-based-predicate-signature ((predicate t) (arguments t)
                                               (reasoner t)) nil)

(defun generate-pattern-variable-dependencies (pattern)
  ;; Produces a list of the variables found in each term.
  (if (quantified-term? pattern) (setq pattern (form pattern))) ;; (TRH)
  (mapcar 'formula-variables pattern))

(defun update-term-state (known-vars pattern-state)
  ;; pattern-entry = (<dependencies> <ask signatures> <term form>)
  ;; pattern-state = (<state> <dependencies> <ask signatures> <term form>)
  (cons
   (derive-pattern-known-state known-vars (cdr pattern-state))
   (cdr pattern-state)))

(defun derive-pattern-known-state (known-vars pattern-entry)
  (mapcar #'(lambda (vars)
              (if (every #'(lambda (var) (member var known-vars)) vars)
                :known
                :unknown))
    (car pattern-entry)))

(defun term-is-feasible? (pattern-state)
  (or (null (third pattern-state)) ;; No specialized source
      (some #'(lambda (ask-signature)
                (satisfies-ask-signature? (car pattern-state)
                                          ask-signature))
            (third pattern-state))))

(defun satisfies-ask-signature? (pattern-data ask-signature)
  (and (eq (car pattern-data) :known) ;; Operator must be known
       (every #'(lambda (arg-state sig-entry)
                  (or (and (eq arg-state :known)
                           (eq sig-entry :input-only))
                      (and (eq arg-state :unknown)
                           (or (eq sig-entry :produces)
                               (eq sig-entry :can-produce)))))
              (cdr pattern-data) ask-signature)))

(defun number-of-vars-bound-by-match (pattern-state)
  (length (vars-bound-by-match pattern-state)))

(defun vars-bound-by-match (pattern-state)
  (let ((var-state (car pattern-state)))
    (cond ((third pattern-state)
           ;; Must match an ask signature, when there is one
           (dolist (ask-signature (third pattern-state) nil)
             (when (satisfies-ask-signature? var-state ask-signature)
               (return-from vars-bound-by-match
                 (values 
                  (remove-duplicates
                   (apply 'append
                          (mapcar #'(lambda (entry dependency)
                                      
                                      (if (eq entry :produces) dependency
                                        nil))
                            ask-signature (cdr (cadr pattern-state))))))))))
          (t ;; Otherwise, assume that the unknown values are found
           ;; by solving it through chaining
           (apply 'append
                  (mapcar #'(lambda (var-state-entry pattern-vars-entry)
                              (if (eq var-state-entry :unknown)
                                pattern-vars-entry))
                    var-state (cadr pattern-state)))))))

(defun number-of-vars-already-bound (pattern-state)
  (let ((n-bound 0))
    (mapc #'(lambda (state-component dependency-component)
              (if (eq state-component :known)
                (incf n-bound (length dependency-component))))
      (car pattern-state) (cadr pattern-state))
    n-bound))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;


(defun test-chainer0 ()
  (fire::create-chainer-from-axioms 
 "Case Construction Knowledge"
 '((data::implies (data::and (data::assertedTermSentences ?concept ?sentence)
                 (data::operatorFormulas ?op ?sentence)
                 (data::uninferredSentence (data::isa ?op data::UninterestingPredicate)))
            (data::caseContainsFact (data::SimpleCaseFn ?concept) ?sentence))   ;; ?? doesn't exist ??
   (data::implies (data::isa ?pred data::MetaKnowledgePredicate)
            (data::isa ?pred data::UninterestingCasePredicate))
   (data::implies (data::isa ?pred data::BookkeepingPredicate)
            (data::isa ?pred data::UninterestingCasePredicate))
   
   )))
  
(defun trace-chainer-internals ()
  (trace derive-feasible-solution-orderings-for-term
         derive-feasible-solution-orderings-for-terms
         predicate-ask-signatures produces-evaluatable-function?
         evaluatable-function? get-lisp-handler quote-if-needed
         fire-evaluatable-function? evaluate do-evaluate-ground
         do-evaluate fire:ask do-query fire:query-within-chainer
         term-is-feasible? derive-pattern-known-state
         update-term-state generate-pattern-variable-dependencies
         pick-best-next-term-candidates find-best-next-term-candidate
         generate-query-order pattern-ask-signatures
         analyze-term-predicate-types argument-based-predicate-signature
         generate-query-order-from-input-signature generate-input-signatures))
       

















;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; End of Code