;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                        -*-
;;;; -------------------------------------------------------------------------
;;;; File name: bc-logic-tests.lsp
;;;;    System: Fire
;;;;    Author: Tom Hinrichs
;;;;   Created: November 17, 2003 09:13:21
;;;;   Purpose: test backchaining logic
;;;;  Modified: Saturday, November 22, 2003 at 09:44:13 by hinrichs
;;;; -------------------------------------------------------------------------

(in-package :cl-user)

(defun trace-bc ()
  #+allegro-ide
  (setf (cg:state (devel::trace-dialog)) :normal)
  (trace fire::do-query fire::query-clause fire::explore-other-terms fire:ask 
         fire::use-single-term-clause fire::applicable-clauses))

;;; use (fire::show-clause-index (first (fire::clause-indexes fire::*kb*)))
;;; to see contents of clause index.

(defvar r nil) ;; For debugging
(defvar a nil)
  
(defun bc-logic-test-reasoner (&optional (title "Backchaining test")) 
  (unless (fire:open-kb? fire:*kb*)
    (setf fire:*kb* nil)      ;; Clear the clause indexes by creating a new kb
    (fire::make-qrg-darpa-kb) ;; Set up KB
    (setf fire:*reasoner* nil))
  (unless fire:*reasoner*
    (setq r (fire:make-reasoner title))
    (fire:in-reasoner r)
    (fire:add-analogy-source r)
    (setq a (car (fire:sources r))))
  (fire::clear-reasoner-clause-indexes)
  (fire::clear-kb-clause-indexes)
  a)

(defun bc-test0 ()
  (bc-logic-test-reasoner)
  (fire:create-clause-index-from-axioms
   "BC Test0"
   '((implies (ante ?X)
              (conse ?X))))
  (fire:add-clause-index-to-reasoner "BC Test0" fire:*reasoner*)
  (ltre:assume! '(ante Foo) :bc-test0))

;;; (fire::query '(conse ?what))

(defun bc-test-conj ()
  (bc-logic-test-reasoner)
  (fire:create-clause-index-from-axioms
   "BC Test Conj"
   '((implies (and (true ?X) (true ?Y))
              (conse ?X ?Y))))
  (fire:add-clause-index-to-reasoner "BC Test Conj" fire:*reasoner*)
  (ltre:assume! '(true Foo) :bc-test-conj)
  (ltre:assume! '(true Bar) :bc-test-conj)
  (ltre:assume! '(not (true Baz)) :bc-test-conj))

;;; (fire::query '(conse Foo Bar))
;;; (fire::query '(conse Foo Baz))

(defun bc-test1 ()
  ;; Tests simple walk-through of clauses
  (bc-logic-test-reasoner)
  (fire:create-clause-index-from-axioms "BC Test1"
                                         '((implies (Human ?x)
                                                    (Mortal ?x))
                                           (implies (Sentient ?x)
                                                    (Human ?x))
                                           (implies (and (Robot ?x)
                                                         (FIRE-based ?x))
                                                    (Sentient ?x))))
  (fire:add-clause-index-to-reasoner "BC Test1" fire:*reasoner*)
  (ltre:assume! '(Human Fred) :bc-test1)
  (ltre:assume! '(Robot Robbie) :bc-test1)
  (ltre:assume! '(FIRE-based Robbie) :ambition))

;;; (fire::query '(Mortal Robbie)) ; => t
;;; (fire::qurey '(Human Robbie))  ; => t
;;; (fire::query '(Mortal ?who))   ; => {Robbie, Fred}
;;; (fire::query '(Sentient ?who)) ; => Robbie

(defun bc-test2 ()
  ;; Tests self-bindings
  (bc-logic-test-reasoner)
  (fire:create-clause-index-from-axioms "Partial Norvig example" 
                                         '((likes ?x ?x)))
  (fire:add-clause-index-to-reasoner "Partial Norvig example" fire:*reasoner*))

;;; (fire::query '(likes Jim Jim))
;;; (fire::query '(likes Jim ?who))

(defun bc-test3 ()
  (bc-logic-test-reasoner)
  (fire:create-clause-index-from-axioms "Reflexive"
                                   '((implies 
                                      (connected ?x ?y)
                                      (connected ?y ?x))
                                     (connected ?z ?z)))
  (fire:add-clause-index-to-reasoner "Reflexive" fire:*reasoner*)
  (ltre:assume! '(connected leg-bone thigh-bone) :bc-test3))

;;; (fire::query '(connected thigh-bone leg-bone))
;;; (fire::query '(connected thigh-bone thigh-bone))

(defun norvig-test ()
  (bc-logic-test-reasoner)
  (fire:create-clause-index-from-axioms 
   "Norvig example" 
   '((implies (likes ?x Cats)
              (likes Sandy ?x))
     (implies (and (likes ?x Lee)
                   (likes ?x Kim))
              (likes Kim ?x))
     (likes ?x ?x)            ;; A simpler world than ours
     (implies (likes ?x ?y)
              (likes ?y ?x))))
  (fire:add-clause-index-to-reasoner "Norvig example" fire:*reasoner*)
  (ltre:assume! '(likes Kim Robin) :book)
  (ltre:assume! '(likes Sandy Lee) :book)
  (ltre:assume! '(likes Sandy Kim) :book)
  (ltre:assume! '(likes Robin Cats) :book))

;;; (fire::query '(likes Sandy ?who)) ; => {Kim Lee Sandy Robin Cats}
;;; (fire::query '(likes Robin Lee))  ; => nil

(defun XOR-test ()
  (bc-logic-test-reasoner)
  (fire:create-clause-index-from-axioms
   "XOR Test"
   '((implies (xor (true ?x)
                   (true ?y))
              (conse ?x ?y))))
  (fire:add-clause-index-to-reasoner "XOR Test" fire:*reasoner*)
  (ltre:assume! '(true Foo) :xor-test)
  (ltre:assume! '(true Bar) :xor-test)
  (ltre:assume! '(not (true Baz)) :xor-test)
  (ltre:assume! '(not (true Bletch)) :xor-test))

;; (fire::query '(conse Foo Bar))    ; => nil
;; (fire::query '(conse Foo Baz))    ; => t
;; (fire::query '(conse Bar Baz))    ; => t
;; (fire::query '(conse Baz Bletch)) ; => nil


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