;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: bc-fib-test.lsp
;;;;    System: FIRE v1
;;;;    Author: Ken Forbus
;;;;   Created: May 28, 2004 10:19:27
;;;;   Purpose: Testing incremental justification of TMS results
;;;; ---------------------------------------------------------------------------
;;;;  Modified: Friday, May 28, 2004 at 22:44:25 by Kenneth Forbus
;;;; ---------------------------------------------------------------------------

(in-package :COMMON-LISP-USER)

;;; This is a lousy way to compute fib, but a great stress-test for the backchainer.

(defun bc-fib-test (&key (aggressive-tms? t))
  ;; Assume reasoner, KB already prepared
  ;; WARNING: Nukes chainers in reasoner!
  ;; Only should be used for stand-alone experiments
  (let ((chainer 
         (fire::create-chainer-from-axioms 
          "Fib chainer"
          '((implies (and (evaluate ?n-2 (DifferenceFn ?n 2))
                          (evaluate ?n-1 (DifferenceFn ?n 1))
                          (fib ?n-2 ?result-2)
                          (fib ?n-1 ?result-1)
                          (evaluate ?result (PlusFn ?result-1 ?result-2)))
                     (fib ?n ?result))))))
    (fire::clear-reasoner-chainers)
    (setq *fib-chainer* chainer)
    ;; Logically, these should be statements that could be included in
    ;; the chainer.  However, the semantics of that is somewhat odd, since
    ;; that looks like a way of hiding facts that should be in the KB.
    (ltre::assume! '(fib 0 1) :base-case)
    (ltre::assume! '(fib 1 1) :base-case)
    (fire::add-chainer-to-reasoner chainer fire::*reasoner*)
    (fire::query '(fib 5 ?answer) :aggressive-tms? aggressive-tms?)))


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