;;;-*-Mode:LISP; Package: CHAOS; Base:10; Syntax:Common-lisp -*-
;;;
;;; Copyright (c) 2000-2018, Toshimi Sawada. All rights reserved.
;;;
;;; Redistribution and use in source and binary forms, with or without
;;; modification, are permitted provided that the following conditions
;;; are met:
;;;
;;;   * Redistributions of source code must retain the above copyright
;;;     notice, this list of conditions and the following disclaimer.
;;;
;;;   * Redistributions in binary form must reproduce the above
;;;     copyright notice, this list of conditions and the following
;;;     disclaimer in the documentation and/or other materials
;;;     provided with the distribution.
;;;
;;; THIS SOFTWARE IS PROVIDED BY THE AUTHOR 'AS IS' AND ANY EXPRESSED
;;; OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
;;; WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
;;; ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
;;; DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
;;; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
;;; GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
;;; INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
;;; WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
;;; NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
;;; SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
;;;
(in-package :chaos)
#|=============================================================================
                               System:CHAOS
                              Module:thstuff
                             File:cexec.lisp
=============================================================================|#
#-(or :chaos-debug SBCL)
(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
#+:chaos-debug
(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))

;;;
(declaim (special $$cexec-term))        ; the target term

;;; *****
;;; RULEs
;;; *****

;;; RULE-PAT
;;; - a rule applicable to the current target
;;; - POS: position matching 
;;; - RULE: the rule
;;; - SUBST: the substitution
;;;
(defstruct (rule-pat (:print-function print-rule-pattern))
  (pos nil :type list)                  ; matched position (list of fixnum)
  (rule nil :type rewrite-rule)         ; matched rule
  (subst nil :type substitution)        ; variable substitution
  (cond-ok t :type (or null t))         ; t iff condition part of the rule is satisfied
  (condition nil :type (or null term))  ; resulting condition part ('if') when cond-ok = nil
  (num 0 :type fixnum)                  ; sequential #, used for debugging
  )

(declaim (type fixnum .rules-so-far.))
(defvar .rules-so-far. 0)

(defun print-rule-pattern (rpat &optional (stream *standard-output*) &rest ignore)
  (declare (type rule-pat rpat)
           (type stream stream)
           (ignore ignore))
  (format stream "~%-- rule pattern: ~d" (rule-pat-num rpat))
  (format stream "~%  posisition: ~a" (rule-pat-pos rpat))
  (format stream "~&  rule      :")(print-chaos-object (rule-pat-rule rpat))
  (format stream "~&  subst     :")(print-substitution (rule-pat-subst rpat))
  (format stream "~&  cond-ok   :~a" (rule-pat-cond-ok rpat))
  (let ((cond (rule-pat-condition rpat)))
    (when cond
      (format stream "~&  condition :")(term-print cond))))

;;; *****
;;; STATE
;;; *****

;;; RWL-STATE
;;; represents a state
;;;
(defstruct (rwl-state
            (:print-function pr-rwl-state))
  (state 0 :type fixnum)                      ; fixnum value identifying this state
  (term nil :type term)                       ; a term
  (trans-rules nil :type list)                ; applicable rules to this state
  (rule-pat nil :type (or null rule-pat))     ; the rule-pat which derived this state
  (subst nil :type list)                      ; list of substitution !!
  (is-final nil :type (or t null))            ; t iff the state is a final state
  (loop nil :type (or t null))                ; t iff the same state occurs more than once
  (condition nil)                             ;
  (depth 0 :type fixnum)                      ; nesting depth of rwl-search*
  )

(declaim (inline state-is-valid-transition))
(defun state-is-valid-transition (state)
  (declare (type rwl-state state)
           (optimize (speed 3) (safety 0)))
  (let ((cond (rwl-state-condition state)))
    (and (not (rwl-state-loop state))
         (or (null cond)
             (is-true? cond)))))

(defun pr-rwl-state (state &optional (stream *standard-output*) &rest ignore)
  (declare (type rwl-state state)
           (type stream stream)
           (ignore ignore))
  (let ((*standard-output* stream))
    (format t "#<rwl-state(~D):" (rwl-state-state state))
    (term-print (rwl-state-term state))
    (princ ", ")
    (dolist (sub (rwl-state-subst state))
      (print-substitution sub))
    (when (rwl-state-is-final state)
      (princ " ,final"))
    (princ ">")))

(declaim (special .rwl-search-depth.)
         (type fixnum .rwl-search-depth.))
(defvar .rwl-search-depth. -1)

(defun print-rwl-state (state &optional (stream *standard-output*) &rest ignore)
  (declare (ignore ignore)
           (type rwl-state state)
           (type stream stream))
  (let ((*standard-output* stream))
    (format t "~%[state ~D-~D] " (rwl-state-depth state) (rwl-state-state state))
    (let ((*print-indent* (+ 4 *print-indent*)))
      (term-print-with-sort (rwl-state-term state))
      (when *cexec-trace*
        (format t "~& matched with the substitution "))
      (let ((*print-indent* (+ 4 *print-indent*)))
        (dolist (subst (rwl-state-subst state))
          (print-next)
          (print-substitution subst)))
      (flush-all))))

(defun print-state-transition (state sub-states &optional (stream *standard-output*))
  (declare (type rwl-state state)
           (type list sub-states)
           (type stream stream))
  (let ((*standard-output* stream)
        (arc-num 0))
    (declare (type fixnum arc-num))
    (format t "~%[state ~D-~D] " (rwl-state-depth state) (rwl-state-state state))
    (term-print-with-sort (rwl-state-term state))
    (dolist (sub sub-states)
      (format t "~&  arc ~D --> [state ~D-~D] " arc-num (rwl-state-depth state) (rwl-state-state sub))
      (let ((*print-indent* (+ 4 *print-indent*)))
        (print-next)
        (print-axiom-brief (rule-pat-rule (rwl-state-rule-pat sub))))
      (incf arc-num))))

;;; ***********
;;; SEARCH TREE
;;; ***********

;;; Search tree
;;; - bi-directional dag (see comlib/dag.lisp)
;;; - datum contains an instance of rwl-state.
;;; 
(defstruct (rwl-sch-node (:include bdag)
            (:conc-name "SCH-NODE-")
            (:print-function pr-rwl-sch-node))
  (done nil :type (or null t))          ; t iff this node is checked already
  (is-solution nil :type (or null t))   ; t iff this node found as a solution
  )

(defmacro create-sch-node (rwl-state)
  `(make-rwl-sch-node :datum ,rwl-state :subnodes nil :parent nil :is-solution nil))

(defun pr-rwl-sch-node (node &optional (stream *standard-output*) &rest ignore)
  (declare (ignore ignore))
  (let ((*standard-output* stream))
    (format t "SCH-NODE:~A" (dag-node-datum node))))

;;; **************
;;; SEARCH CONTEXT
;;; **************

;;; RWL-SCH-CONTEXT
;;; 
(defstruct (rwl-sch-context
            (:print-function print-sch-context))
  (module nil :type module)                   ; context module
  (term nil :type term)                       ; initial term
  (pattern nil :type term)                    ; pattern to be matched
  (condition nil :type (or null term))        ; =(*)=> with COND
  (zero-trans-allowed nil :type (or null t))  ; ... =>*
  (final-check nil :type (or null t))         ; ... =>!
  (max-sol most-positive-fixnum :type fixnum) ; =(max-sol, )=>
  (sol-found 0 :type fixnum)                  ; found solutions so far
  (max-depth most-positive-fixnum :type fixnum)
                                        ; =(, max-depth)=>
  (cur-depth 0 :type fixnum)            ; current depth
  (root nil :type (or null rwl-sch-node)) ; root node of the search tree
                                        ;   (an instance of rwl-sch-node) 
  (trans-so-far 0 :type fixnum)         ; # of transitions so far
  (last-siblings nil :type list)        ; nodes to be checked
                                        ; initially, this contains the root.
  (state-predicate nil)                 ; STATE equality predicate
  (answers nil :type list)              ; list of STATEs satisfying specified
                                        ; conditions.
  (bind nil)                            ; ....
  (if nil)                              ;
  (pr-out? nil :type (or null t))       ;
  (term-hash nil :type simple-vector)   ; term hash table for catching loop
  )

(defun print-sch-context (ctxt &optional (stream *standard-output*) &rest ignore)
  (declare (type rwl-sch-context ctxt)
           (type stream stream)
           (ignore ignore))
  (let ((*standard-output* stream)
        (mod (rwl-sch-context-module ctxt)))
    (with-in-module (mod)
      (format t "~%<< sch context >>")
      (format t "~%   module: ")
      (print-chaos-object (rwl-sch-context-module ctxt))
      (format t "~%   term: ")
      (term-print-with-sort (rwl-sch-context-term ctxt))
      (format t "~%   pattern: ")
      (term-print-with-sort (rwl-sch-context-pattern ctxt))
      (format t "~%   condition: ")
      (if (rwl-sch-context-condition ctxt)
          (term-print-with-sort (rwl-sch-context-condition ctxt))
        (princ "None."))
      (format t "~%   zero?: ~A" (rwl-sch-context-zero-trans-allowed ctxt))
      (format t "~%   final?: ~A" (rwl-sch-context-final-check ctxt))
      (format t "~%   max sol. : ~D" (rwl-sch-context-max-sol ctxt))
      (format t "~%   solutions: ~D" (rwl-sch-context-sol-found ctxt))
      (format t "~%   max depth: ~D" (rwl-sch-context-max-depth ctxt))
      (format t "~%   current depth: ~D" (rwl-sch-context-cur-depth ctxt))
      (format t "~%   root node: ~A" (rwl-sch-context-root ctxt))
      ;; (format t "~%   states: ~D" (rwl-sch-context-states-so-far ctxt))
      (format t "~%   transitions: ~D" (rwl-sch-context-trans-so-far ctxt))
      (format t "~%   last siblings: ")
      (dolist (s (rwl-sch-context-last-siblings ctxt))
        (format t "~%     ~A" s))
      (format t "~%   answers: ")
      (dolist (x (reverse (rwl-sch-context-answers ctxt)))
        (term-print-with-sort (rwl-state-term x)))
      (when (rwl-sch-context-bind ctxt)
        (format t "~%   bind pattern: ")
        (term-print-with-sort (rwl-sch-context-bind ctxt)))
      (when (rwl-sch-context-if ctxt)
        (format t "~%   if: ")
        (term-print-with-sort (rwl-sch-context-if ctxt))))))


;;; ******************
;;; RWL-SCH-NODE utils
;;; ******************

;;; print the rule & state
;;;
(defun show-rwl-sch-state (dag &optional (path? t) (bind-pattern nil))
  (declare (type rwl-sch-node dag))
  (let* ((st (dag-node-datum dag))
         (term (rwl-state-term st))
         (rule-pat (rwl-state-rule-pat st))
         (rl (if rule-pat (rule-pat-rule rule-pat)
               nil)))
    (when (and rl path?)
      (print-next)
      (princ "  ")
      (let ((*print-indent* (+ 8 *print-indent*)))
        (print-chaos-object rl) ; (print-axiom-brief rl)
        ))
    (format t "~%[state ~D-~D] " (rwl-state-depth st) (rwl-state-state st))
    (term-print-with-sort term)
    (dolist (sub (rwl-state-subst st))
      (format t "~&    ")
      (print-substitution sub)
      (when bind-pattern
        (let ((bimage (substitution-image-simplifying sub bind-pattern)))
          (normalize-term bimage)
          (format t "~%    => ")
          (term-print-with-sort bimage))))))

;;; print the label of a rule which derived a state
;;; that denode contains.
;;;
(defun show-rwl-sch-label (dnode)
  (declare (type rwl-sch-node dnode))
  (let* ((dt (dag-node-datum dnode))
         (rl (rule-pat-rule (rwl-state-rule-pat dt)))
         (label (car (rule-labels rl))))
    (if label
        (format t "~&[~a]" label)
      (format t "~&NONE"))))


;;; RULE PAT constructor
(defun make-rule-pat-with-check (pos rule subst sch-context)
  (declare (type list pos)
           (type rewrite-rule rule)
           (type substitution subst)
           (type rwl-sch-context sch-context)
           (optimize (speed 3) (safety 0)))
  (when (rule-non-exec rule)
    ;; the rule is marked as non-executable
    (return-from make-rule-pat-with-check nil))
  (let ((condition (rule-condition rule)))
    (declare (type term condition))
    ;; pre check whether the condition part is satisfied or not
    (when (and (is-true? condition)
               (null (rule-id-condition rule)))
      ;; rule is not conditional
      (return-from make-rule-pat-with-check
        (make-rule-pat :pos pos :rule rule :subst subst :num (incf .rules-so-far.))))
    ;; check the condition
    (let (($$term nil)
          ($$cond (set-term-color (substitution-image-cp subst condition))))
      (when *cexec-debug*
        (format t "~%rule: cond ") (term-print-with-sort $$cond)
        (format t "~%      subst") (print-substitution subst)
        (let ((vars (term-variables $$cond)))
          (dolist (v vars)
            (format t "~% var ") (term-print-with-sort v))))
      (catch 'rule-failure
        (if (and (or (null (rule-id-condition rule))
                     (rule-eval-id-condition subst
                                             (rule-id-condition rule)
                                             :slow))
                 (is-true? (progn (normalize-term $$cond) $$cond)))
            ;; the condition is satisfied
            (return-from make-rule-pat-with-check 
              (make-rule-pat :pos pos :rule rule :subst subst :cond-ok t :condition $$cond :num (incf .rules-so-far.)))
          (if (rwl-sch-context-if sch-context)
              ;; rule condition fail & there exists 'if'
              (return-from make-rule-pat-with-check
                (make-rule-pat :pos pos :rule rule :subst subst :cond-ok nil :condition $$cond :num (incf .rules-so-far.)))
            (return-from make-rule-pat-with-check nil))))
      nil)))

(defun rule-pat-equal (pat1 pat2)
  (declare (type rule-pat pat1 pat2)
           (optimize (speed 3) (safety 0)))
  (and (equal (rule-pat-pos pat1) (rule-pat-pos pat2))
       (eq (rule-pat-rule pat1) (rule-pat-rule pat2))
       (substitution-equal (rule-pat-subst pat1) (rule-pat-subst pat2))))


;;; *********************
;;; SEARCH CONTEXT UTILS
;;; *********************

;;; parse-depth&state
;;;
(defun parse-depth&state (&optional ds-string)
  (unless ds-string
    (return-from parse-depth&state nil))
  (let* ((ds-list (parse-with-delimiter ds-string #\-))
         (depth (or (and (cdr ds-list) (read-from-string (car ds-list)))
                    0))
         (state (or (and (cdr ds-list) (read-from-string (cadr ds-list)))
                    (read-from-string (car ds-list)))))
    (unless (and (integerp depth) (>= depth 0)
                 (integerp state) (>= state 0))
      (with-output-chaos-error ('invalid-depth-state)
        (format t "Invalid depth/state specifier: ~a" ds-string)))
    (list depth state)))

;;; show-rwl-sch-graph
;;;
(defun show-rwl-sch-graph (&optional num)
  (let ((c-num (if num
                   (read-from-string num)
                 0))
        (sch-context nil))
    (unless (integerp c-num)
      (with-output-chaos-error ('invalid-context-number)
        (format t "invalid search graph number ~s" num)))
    (setq sch-context (nth c-num (reverse .rwl-context-stack.)))
    (unless sch-context
      (with-output-chaos-error ('no-such-context)
        (format t "no such search graph ~d" num)))
    (let ((mod (rwl-sch-context-module sch-context))
          (root (rwl-sch-context-root sch-context)))
      (unless mod
        (with-output-chaos-error ('no-context)
          (format t "no context module...")))
      (unless root
        (with-output-chaos-error ('no-root)
          (format t "no search result exists...")))
      (when (and *current-module*
                 (not (eq *current-module* mod)))
        (with-output-chaos-warning ()
          (format t "the context(module) of search graph is different from the current module.")))
      ;;
      (with-in-module (mod)
        (let ((state-hash (make-hash-table)))
          (dag-wfs root
                   #'(lambda (d)
                       (let* ((state-node (dag-node-datum d))
                              (state (rwl-state-state state-node)))
                         (unless (gethash state state-hash)
                           (setf (gethash state state-hash) t)
                           (print-state-transition
                            state-node
                            (mapcar #'(lambda (sd)
                                        (dag-node-datum sd))
                                    (dag-node-subnodes d))))))))))))

(defun find-rwl-sch-state (num &optional (sch-context .rwl-sch-context.))
  (declare (type fixnum num))
  (unless sch-context
    (with-output-chaos-error ('no-root-node)
      (format t "no search result exists")))
  (let ((dag nil))
    (setq dag
      (catch 'dag-found
        (dag-wfs (rwl-sch-context-root sch-context)
                 #'(lambda (d)
                     (let ((st (dag-node-datum d)))
                       (when (= (rwl-state-state st) num)
                         (throw 'dag-found d)))))
        nil))
    dag))

(defun find-rwl-sch-state-globally (num)
  (declare (type fixnum num))
  (dolist (context .rwl-context-stack.)
    (let ((st (find-rwl-sch-state num context)))
      (when st (return-from find-rwl-sch-state-globally (values context st))))))

(defun show-rwl-sch-path (&optional (ds-string nil)
                                    (label? nil)
                                    (state-only? nil))

  (unless ds-string
    (return-from show-rwl-sch-path
      (format t "~%Nothing to be reported...")))
  (unless .rwl-context-stack.
    (with-output-chaos-error ('no-context)
      (format t "~%There is no search context.")))
  (let* ((ds-list (parse-depth&state ds-string))
         (sch-context (or (nth (car ds-list) (reverse .rwl-context-stack.))
                          (with-output-chaos-error ('no-sch-context)
                            (format t "There is no RWL search context ~d" (car ds-list)))))
         (dag (find-rwl-sch-state (cadr ds-list) sch-context)))
    (unless dag
      (with-output-chaos-error ('no-such-state)
        (format t "There is no state ~d in context ~d" (cadr ds-list) (car ds-list))))
    (let ((mod (rwl-sch-context-module sch-context)))
      (when (and *current-module*
                 (not (eq *current-module* mod)))
        (with-output-chaos-warning ()
          (format t "the context(module) of search result is different from the current module.")))
      (with-in-module (mod)
        (cond (state-only? (show-rwl-sch-state dag nil (rwl-sch-context-bind sch-context)))
              (t (let ((parents (get-bdag-parents dag)))
                   (cond (label?
                          (dolist (p (cdr parents)) ;root has no transition
                            (show-rwl-sch-label p))
                          (show-rwl-sch-label dag))
                         (t (dolist (p parents)
                              (show-rwl-sch-state p t (rwl-sch-context-bind sch-context)))
                            (show-rwl-sch-state dag t (rwl-sch-context-bind sch-context)))))))))))

;;; ******************
;;; SOME UTILs on TERM
;;; ******************
;;; returns a subterm at position 'pos'
;;;
(declaim (inline get-target-subterm))
(defun get-target-subterm (term pos)
  (declare (type term term)
           (type list pos)
           (optimize (speed 3) (safety 0)))
  (let ((cur term))
    (declare (type term cur))
    (when pos
      (dolist (p pos)
        (declare (type fixnum p))
        (setq cur (term-arg-n cur p))
        (unless cur
          (with-output-panic-message ()
            (format t "could not find subterm at pos ~d" pos)
            (format t "~% target was ")
            (term-print term)
            (break "wow!")
            (chaos-error 'panic)))))
    cur))

;;; *************
;;; PATTERN MATCH
;;; *************

;;; finds all transition rules possibly applicable to the given target term
;;;
(defun find-matching-rules-for-exec (target sch-context &optional start-pos)
  (declare (type term target)
           (type rwl-sch-context sch-context)
           (type list start-pos)
           (optimize (speed 3) (safety 0)))
  (let ((module (rwl-sch-context-module sch-context)))
    (declare (type module module))
    (when start-pos
      (setq target (get-target-subterm target start-pos)))
    (with-in-module (module)
      (let* ((*module-all-rules-every* t)
             (rules (get-module-axioms *current-module* t))
             (rls nil)
             (res nil))
        (declare (type list res))
        (dolist (rule rules)
          (declare (type rewrite-rule rule))
          (when (rule-is-rule rule)
            (push rule rls)))
        ;; gather rules
        (setq res (find-matching-rules-for-exec* target rls start-pos sch-context))
        (setq res (delete-duplicates res
                                     :test #'rule-pat-equal))
        (when *cexec-debug*
          (format t "~%** ~D rules were found for term: "
                  (length res))
          (term-print target)
          (terpri)
          (dolist (r res)
            (print-rule-pattern r)))
        res ))))

(defun find-matching-rules-for-exec* (target rules pos sch-context)
  (declare (type term target)
           (type list rules pos)
           (type rwl-sch-context sch-context))
  (when *cexec-debug*
    (format t "~%find matching rules. ")
    (term-print target)
    (terpri))
  (if (term-is-application-form? target)
      (let ((res nil)
            (rule-pat nil))
        (do* ((rls rules (cdr rls))
              (rule (car rls) (car rls)))
            ((endp rls))
          (let* ((patterns nil)
                 (lhs (rule-lhs rule))
                 (head (if (term-is-variable? lhs)
                           nil
                         (term-head lhs))))
            (push rule patterns)
            ;; ------- apply-rule always applies extensions
            (when head
              (when (method-is-associative head)
                (if (method-is-commutative head)
                    (let ((ac-ext (give-AC-extension rule)))
                      (when ac-ext
                        (unless (car ac-ext)
                          (print ac-ext)
                          (break "Here it is!"))
                        (push (car ac-ext) patterns)))
                  ;;
                  (let ((a-exts (give-A-extensions rule)))
                    (dolist (r a-exts)
                      (when r
                        (push r patterns)))))))
            ;; ------------
            (dolist (pat patterns)
              (block next
                (unless pat (break "HANA my"))
                ;; find all possible subst
                (multiple-value-bind (gs sub no-match eeq)
                    (@matcher (axiom-lhs pat) target :match)
                  (declare (ignore eeq))
                  (when no-match (return-from next))
                  (setq rule-pat (make-rule-pat-with-check pos pat sub sch-context))
                  (when rule-pat
                    (push rule-pat res))
                  (loop
                    (multiple-value-setq (gs sub no-match)
                      (next-match gs))
                    (when no-match (return-from next))
                    (setq rule-pat (make-rule-pat-with-check pos pat sub sch-context))
                    (when rule-pat
                      (push rule-pat res))))))
            ))                          ; done for all rules
        ;; recursively find rules for subterms
        (dotimes (x (length (term-subterms target)))
          (let ((r (find-matching-rules-for-exec* (term-arg-n target x)
                                                  rules
                                                  (append pos (list x))
                                                  sch-context)))
            (when r (setq res (nconc res r)))))
        ;;
        res)
    nil))

;;; ****************
;;; SOLUTION CHECKER
;;; ****************

(declaim (inline if-binding-should-be-printe))
(defun if-binding-should-be-printed (sch-context)
  (declare (type rwl-sch-context sch-context)
           (optimize (speed 3) (safety 0)))
  (and (rwl-sch-context-if sch-context)
       (<= (rwl-sch-context-cur-depth sch-context) (rwl-sch-context-max-depth sch-context))))

;;; 
(declaim (inline print-subst-if-binding-result))
(defun print-subst-if-binding-result (state sub sch-context)
  (declare (ignore state)
           (optimize (speed 3) (safety 0)))
  (setf (rwl-sch-context-pr-out? sch-context) t)
  (print-next)
  (format t "    ") (print-substitution sub)
  (when (rwl-sch-context-bind sch-context)
    (let ((bimg (substitution-image-simplifying sub (rwl-sch-context-bind sch-context))))
      (normalize-term bimg)
      (print-next)
      (format t "    --> ")
      (if (and *grind-bool-term*
               (sort= (term-sort bimg) *bool-sort*))
          (let ((bt (abstract-boolean-term bimg *current-module*)))
            (print-bterm-grinding bt))
        (term-print-with-sort bimg)))))

;;; rwl-sch-check-conditions (node rwl-sch-context)
;;; check if the given state matches to the target pattern.
;;; return t iff matches, otherwise nil.
;;;
(defun rwl-sch-check-conditions (node sch-context)
  (declare (type rwl-sch-node node)
           (type rwl-sch-context sch-context)
           (optimize (speed 3) (safety 0)))
  (flet ((condition-check-ok (subst)
           (let ((cond (rwl-sch-context-condition sch-context))
                 ($$term nil)
                 ($$cond nil)
                 (*rewrite-exec-mode* (if *rewrite-exec-condition*
                                          *rewrite-exec-mode*
                                        nil)))
             (if (null cond)
                 (setq $$cond *bool-true*)
               (setq $$cond (set-term-color
                             (substitution-image-cp subst cond))))
             (when *cexec-debug*
               (format t "~%  subst     :") (print-substitution subst)
               (format t "~&  suchThat  :") (term-print $$cond))
             (or (is-true? $$cond)
                 (is-true? (progn
                             (if *cexec-debug*
                                 (let (($$trace-rewrite t))
                                   (print-term-tree $$cond t)
                                   (normalize-term $$cond))
                               (normalize-term $$cond))
                             (when *cexec-debug*
                               (format t " -C-> ") (term-print $$cond)
                               (format t "~% = ~s" (is-true? $$cond)))
                             $$cond))))))
    ;; if checked already, we return immediately as non.
    (when (and (sch-node-done node) (null (rwl-sch-context-if sch-context)))
      (return-from rwl-sch-check-conditions nil))
    ;;
    (let* ((state (dag-node-datum node))
           (if-var (rwl-sch-context-if sch-context))
           (rule-pat (rwl-state-rule-pat state)))
      (declare (type rwl-state state))

      (when *chaos-verbose*
        (format t " ~D-~D" (rwl-state-depth state) (rwl-state-state state)))

      (setf (sch-node-done node) t)     ; mark checked already

      (when *cexec-debug* 
        (when (rwl-sch-context-condition sch-context)
          (format t "~%** check condition ")
          (term-print-with-sort (rwl-sch-context-condition sch-context))
          (if rule-pat
              (print-rule-pattern rule-pat)
            (format t "~% no rule-pat."))))
      ;; 0 transition?
      (when (and (not (rwl-sch-context-zero-trans-allowed sch-context))
                 (= 0 (rwl-sch-context-trans-so-far sch-context)))
        (when *cexec-debug*
          (format t "~%.check condition return with 0 transition."))
        (return-from rwl-sch-check-conditions nil))
      ;; check with target pattern.
      (multiple-value-bind (gs sub no-match eeq)
          (@matcher (rwl-sch-context-pattern sch-context)
                    (rwl-state-term state)
                    :match)
        (declare (ignore eeq))
        (when no-match
          (when *cexec-debug*
            (format t "~%.check condition return with no-match."))
          (return-from rwl-sch-check-conditions nil))
        ;; expand subst with 
        (let ((rule-subst (and rule-pat (rule-pat-subst rule-pat))))
          (when (car rule-subst)
            (setq sub (append sub rule-subst))))
        ;; additionaly expand subst 'if' part bindings
        (when if-var
          (setq sub (substitution-add sub if-var (or (rwl-state-condition state)
                                                     *bool-true*))))
        (when (condition-check-ok sub)
          (when (if-binding-should-be-printed sch-context) ; if-var
            (pr-used-rule state)
            (print-subst-if-binding-result state sub sch-context))
          (when (state-is-valid-transition state)
            (push sub (rwl-state-subst state))))
        ;; try other patterns untill there's no hope
        (loop
          (multiple-value-setq (gs sub no-match)
            (next-match gs))
          (when no-match (return))
          ;; expand subst with 
          (let ((rule-subst (and rule-pat (rule-pat-subst rule-pat))))
            (when (car rule-subst)
              (setq sub (append sub rule-subst))))
          (when if-var
            (setq sub (substitution-add sub if-var (or (rwl-state-condition state)
                                                       *bool-true*))))
          (when (condition-check-ok sub)
            (when (if-binding-should-be-printed sch-context) ; if-var
              (when (pr-used-rule state)
                (print-subst-if-binding-result state sub sch-context)))
            (when (state-is-valid-transition state)
              (push sub (rwl-state-subst state))))))
      (not (null (rwl-state-subst state))))))

(defun pr-used-rule (state)
  (declare (type rwl-state state))
  (let ((rule-pat (rwl-state-rule-pat state))
        (rule nil))
    (unless rule-pat (return-from pr-used-rule nil))
    (setq rule (rule-pat-rule rule-pat))
    (unless *print-exec-rule*
      (when (member (axiom-kind rule) .ext-rule-kinds.)
        (return-from pr-used-rule nil)))
    (unless *rwl-search-no-state-report*
      (format t "~%=> ")
      (print-axiom-brief rule))
    t))

;;; *********
;;; TERM HASH : used for loop check
;;; *********
(defvar .cexec-term-hash. nil)
;; (deftype term-hash-key () '(unsigned-byte 29))
(deftype term-hash-key () 'fixnum)
#+(or (and :SBCL :64-BIT) (and :ALLEGRO :64BIT))
(defconstant term-hash-mask #x1FFFFFFFFFFFFFF)
#+(or (and :SBCL :32-BIT) (and :ALLEGRO :32BIT))
(defconstant term-hash-mask #x1FFFFFFF)
#-(or :SBCL :ALLEGRO)
(defconstant term-hash-mask #x1FFFFFFF)

(defconstant term-hash-size 9001)

(declaim (inline term-hash-equal))
#-CMU
(defun term-hash-equal (x)
  (declare (optimize (speed 3) (safety 0)))
  (logand term-hash-mask (sxhash x)))

#+CMU
(defun term-hash-equal (x)
  (sxhash x))

(declaim (inline term-hash-eq))
(defun term-hash-eq (object)
  (declare (optimize (speed 3) (safety 0)))
  (ash (+ (the term-hash-key
	    (logand term-hash-mask
		    (the fixnum (addr-of object))))
	  3)
       -3))

(declaim (inline term-hash-comb))
(defun term-hash-comb (x y)
  (declare (optimize (speed 3) (safety 0))
           (type fixnum x y))
  (the term-hash-key (logand term-hash-mask (logand term-hash-mask (+ x y)))))

(defun cexec-hash-term (term)
  (declare (type term term)
           (optimize (speed 3) (safety 0)))
  (cond ((term-is-applform? term)
         (let ((res (sxhash (the symbol (method-id-symbol (term-head term))))))
           (dolist (subterm (term-subterms term))
             (setq res (term-hash-comb res (cexec-hash-term subterm))))
           res))
        ((term-is-builtin-constant? term)
         (term-hash-comb (sxhash (the symbol (sort-id (term-sort term))))
                         (term-hash-equal (term-builtin-value term))))
        ((term-is-variable? term) (term-hash-eq term))))

; (defun dump-cexec-term-hash (&optional (size term-hash-size))
;   (let ((mod (get-context-module)))
;     (unless mod (return-from dump-cexec-term-hash nil))
;     (with-in-module (mod)
;       (dotimes (x size)
;         (let ((ent (svref .cexec-term-hash. x)))
;           (when ent
;             (format t "~%[~3d]: ~d entrie(s)" x (length ent))
;             (dotimes (y (length ent))
;               (let ((e (nth y ent)))
;                 (format t "~%(~d)" y)
;                 (let ((*print-indent* (+ 2 *print-indent*)))
;                   (term-print (car e))
;                   (print-next)
;                   (princ "==>")
;                   (print-next)
;                   (term-print (cdr e)))))))))))

(defun dump-cexec-term-hash (&optional (size term-hash-size))
  (let ((mod (get-context-module)))
    (unless mod (return-from dump-cexec-term-hash nil))
    (with-in-module (mod)
      (dotimes (x size)
        (let ((ent (svref .cexec-term-hash. x)))
          (when ent
            (format t "~%[~3d]: ~d entrie(s)" x (length ent))
            (dotimes (y (length ent))
              (let ((e (nth y ent)))
                (format t "~%(~d) " y) 
                (term-print (car e))
                (print-next)
                (princ "==> ")
                (princ (cdr e))))))))))

(declaim (inline get-sch-hashed-term))
(defun  get-sch-hashed-term (term term-hash)
  (declare (type term term)
           (type simple-vector term-hash)
           (optimize (speed 3) (safety 0)))
 (let ((val (cexec-hash-term term)))
   (let* ((ent (svref term-hash
                      (mod val term-hash-size)))
          (val (cdr (assoc term ent :test #'term-equational-equal))))
     (when val (incf (the fixnum *term-memo-hash-hit*)))
     val)))

(declaim (inline set-sch-hashed-term))
(defun set-sch-hashed-term (term term-hash value)
  (declare (type term term)
           (type simple-vector term-hash)
           (type fixnum value)
           (optimize (speed 3) (safety 0)))
  (let ((val (cexec-hash-term term)))
    (let ((ind (mod val term-hash-size)))
      (let ((ent (svref term-hash ind)))
        (let ((pr (assoc term ent :test #'term-equational-equal)))
          (if pr (rplacd pr value)
            (setf (svref term-hash ind) (cons (cons term value) ent))))))))

(defmacro cexec-get-hashed-term (term)
  `(get-sch-hashed-term ,term .cexec-term-hash.))

(defmacro cexec-set-hashed-term (term state-num)
  `(set-sch-hashed-term ,term .cexec-term-hash. ,state-num))

(declaim (inline cexec-sch-check-predicate))
(defun cexec-sch-check-predicate (term t1 pred-pat)
  (declare (type term term t1)
           (type list pred-pat)
           (optimize (speed 3) (safety 0)))
  (let ((pred (car pred-pat))
        (vars (cdr pred-pat))
        (subst nil)
        (res nil))
    (declare (type term pred)
             (type list vars))
    ;; make substittion
    (if (sort<= (term-sort term) (term-sort (the term (car vars))) *current-sort-order*)
        (push (cons (car vars) term) subst)
      (with-output-chaos-error ('invalid-state)
        (format t "withStateEq: sort of term does not match with variable:")
        (format t "~%  variable: ")
        (term-print-with-sort (car vars))
        (format t "~%  term:  ")
        (term-print-with-sort term)))
    (if (sort<= (term-sort term) (term-sort (cadr vars)) *current-sort-order*)
        (push (cons (cadr vars) t1) subst)
      (with-output-chaos-error ('invalid-state)
        (format t "withStateEq: sort of term does not match with variable:")
        (format t "~%  variable: ")
        (term-print-with-sort (cadr vars))
        (format t "~%  term: ")
        (term-print-with-sort t1)))
      
    ;; apply subst with coping pred
    ;; then reduce
    (setq res
      (is-true?
       (let (($$cond (set-term-color
                      (substitution-image-cp subst pred)))
             (*rewrite-exec-mode*
              (if *rewrite-exec-condition*
                  *rewrite-exec-mode*
                nil)))
         (when *cexec-debug* 
           (format t "~%[withEQ] ")
           (term-print $$cond))
         (normalize-term $$cond)
         (when *cexec-debug*
           (format t "~% = ")
           (term-print $$cond))
         $$cond)))
    (when (and res *cexec-trace*)
      (format t "~%** state predicate returned `true'."))
    res))

(defun cexec-loop-check (term sch-context)
  (declare (type term)
           (type rwl-sch-context sch-context)
           (optimize (speed 3) (safety 0)))
  (or (get-sch-hashed-term term .cexec-term-hash.)
      (let ((pred-pat (rwl-sch-context-state-predicate sch-context)))
        (if pred-pat
            (dotimes (x term-hash-size nil)
              (declare (fixnum x))
              (let ((entry (svref .cexec-term-hash. x)))
                (when entry
                  (dotimes (y (length entry))
                    (declare (type fixnum y))
                    (let ((t1 (nth y entry)))
                      (when (cexec-sch-check-predicate term (car t1) pred-pat)
                        (return-from cexec-loop-check (cdr t1))))))))
          nil))))

;;; 
;;; MAKE-RWL-STATE-WITH-HASH
;;;
(defun make-rwl-state-with-hash (target rule-pat sch-context)
  (declare (type term target)
           (type rule-pat rule-pat)
           (type rwl-sch-context sch-context)
           (optimize (speed 3) (safety 0)))
  (let* ((ostate-num (cexec-loop-check target sch-context))
         (condition (rule-pat-condition rule-pat))
         (new-state nil))
    (declare (type (or null fixnum) ostate-num))
    (cond (ostate-num
           ;; this means the same state has alredy been generated
           ;; from a node other than this node.
           ;; we create brand new state with the same state number
           (setq new-state (make-rwl-state :state ostate-num
                                           :term  target
                                           :rule-pat  rule-pat
                                           :subst  nil
                                           :condition condition
                                           :depth .rwl-search-depth.))
           (when (or *cexec-trace* *chaos-verbose*)
             (format t "~%* loop"))
           (setf (rwl-state-loop new-state) t))
          (t  (let ((state-num (incf .rwl-states-so-far.)))
                (setq new-state (make-rwl-state :state state-num
                                                :term  target
                                                :rule-pat  rule-pat
                                                :subst  nil
                                                :condition  condition
                                                :depth .rwl-search-depth.))
                ;; register the term
                (when *cexec-debug*
                  (format t "~%** hashing state ~D" state-num))
                (set-sch-hashed-term target .cexec-term-hash. state-num))))
    ;;
    new-state))

;;; *******************
;;; ONE STEP TRANSITION
;;; *******************

;;; RWL-STATE-SET-TRANSITION-RULES
;;;
(defun rwl-state-set-transition-rules (state sch-context)
  (declare (type rwl-state state)
           (type rwl-sch-context sch-context)
           (optimize (speed 3) (safety 0)))
  (let ((rule-pats (find-matching-rules-for-exec (rwl-state-term state) sch-context)))
    (setf (rwl-state-trans-rules state) rule-pats)
    (unless rule-pats
      (setf (rwl-state-is-final state) t))))

;;;
;;; APPLY-RULE-CEXEC: rule target -> Bool
;;;
(defun apply-rule-cexec (rule term subst)
  (declare (type rewrite-rule rule)
           (term term)
           (substitution subst))
  (catch 'rule-failure
    (progn
      (term-replace-dd-simple
       term
       (set-term-color
        (substitution-image-simplifying subst
                                        (rule-rhs rule)
                                        (rule-need-copy rule)
                                        :slow)))
      (return-from apply-rule-cexec t)))
  nil)

;;; CEXEC-TERM-1 (state-as-dag)
;;;
;;; - compute all possible transitions from the given state(an instance of
;;;   rwl-sch-node).
;;; - returns the list of substates which derived from the given state.
;;; - NOTE: term of the given state is NOT modified.
;;;
(defun cexec-term-1 (dag sch-context)   ; node-num ...
  (declare (type rwl-sch-node dag)
           (type rwl-sch-context sch-context)
           (optimize (speed 3) (safety 0)))
  (let* ((state (dag-node-datum dag))
         (term (rwl-state-term state)))
    (declare (type rwl-state state)
             (type term term))
    (flet ((no-more-transition ()
             (when (or *cexec-trace* *chaos-verbose*)
               (when (and (term-is-applform? term)
                          (method-has-trans-rule (term-head term)))
                 (with-output-simple-msg ()
                   (format t "-- no more transitions from state ~D-~D."
                           (rwl-state-depth state)
                           (rwl-state-state state)))))
             (setf (rwl-state-is-final state) t)
             nil)
           (exec-trace-form ()
             (format t "=(~a,~a)=>~a"
                     (if (= (rwl-sch-context-max-sol sch-context)
                            most-positive-fixnum)
                         "*"
                       (rwl-sch-context-max-sol sch-context))
                     (rwl-sch-context-cur-depth sch-context)
                     (if (rwl-sch-context-final-check sch-context)
                         "!"
                       (if (rwl-sch-context-zero-trans-allowed sch-context)
                           "*"
                         "+"))))
           (state-is-valid? (state)
             (let ((cond (rwl-state-condition state)))
               (or (null cond) (is-true? cond)))))
      ;;
      (unless (state-is-valid? state)
        (return-from cexec-term-1 nil))
      ;;
      (let ((xterm term)
            (ptrans? (dag-node-subnodes dag)))
        (when *cexec-debug*
          (format t "~%[cexec-term-1] target = ")
          (let ((*fancy-print* nil))
            (term-print-with-sort xterm))
          (flush-all))
        ;; already computed ..
        (when ptrans? (return-from cexec-term-1 ptrans?))
        ;;
        ;; apply all rules found
        ;;
        (let ((rule-pats (rwl-state-trans-rules state))
              (*rewrite-exec-mode* t)
              (sub-states nil)
              (real-pats nil))
          (setq real-pats (remove-if #'(lambda (x) (not (rule-pat-cond-ok x))) rule-pats))
          (when *cexec-debug*
            (format t "~%++ ~D rule patterns for state" (length rule-pats))
            (pr-rwl-state state))
          (when *chaos-verbose*
            (format t "~%-- from [state ~D-~D] "
                    (rwl-state-depth state)
                    (rwl-state-state state))
            (format t "~D possible transitions....."
                    (length real-pats)))
          ;;
          (unless rule-pats
            ;; no rules
            (no-more-transition)
            (return-from cexec-term-1 nil))
          ;; 
          (when *cexec-trace*
            (flush-all)
            (format t "~%~%**> Step ~D from [state ~D-~D] "
                    (rwl-sch-context-cur-depth sch-context)
                    (rwl-state-depth state)
                    (rwl-state-state state))
            (term-print-with-sort (rwl-state-term state))
            (flush-all))
          ;; apply all possible rules
          (do* ((rls rule-pats (cdr rls))
                (rule-pat (car rls) (car rls)))
              ((null rule-pat))
            (let* ((target-whole (simple-copy-term xterm))
                   (target (get-target-subterm target-whole
                                               (rule-pat-pos rule-pat))))
              (declare (type term target-whole)
                       (type term target))
              ;; the following should be done iff the target is NOT
              ;; in hash table + register target in hash.
              (when (apply-rule-cexec (rule-pat-rule rule-pat)
                                      target
                                      (rule-pat-subst rule-pat))
                (incf (rwl-sch-context-trans-so-far sch-context))
                (when *cexec-normalize*
                  (when *cexec-debug*
                    (format t "~%.. start doing normalization because cexec normalize is on.~%  -- ")
                    (term-print target-whole))
                  (let ((*rewrite-exec-mode* nil)
                        (xterm (if (and *cexec-trace* *chaos-verbose*)
                                   (simple-copy-term target-whole)
                                 nil)))
                    (mark-term-as-not-lowest-parsed target-whole)
                    (reset-reduced-flag target-whole)
                    (rewrite* target-whole)
                    (when *cexec-debug*
                      (format t "~&==> ")
                      (term-print target-whole))
                    (when xterm
                      (print-next)
                      (unless (term-equational-equal xterm target-whole)
                        (flush-all)
                        (let ((*fancy-print* nil)
                              (*print-indent* (+ 4 *print-indent*)))
                          (princ "> pre normalization : ")
                          (term-print xterm)
                          (print-next)
                          (princ "== ")
                          (term-print target-whole))
                        (flush-all)))))
                (let ((sub-state (make-rwl-state-with-hash target-whole
                                                           rule-pat
                                                           sch-context)))
                  (declare (type rwl-state sub-state))
                  (when sub-state
                    (when *cexec-debug*
                      (format t "~%** used rule pat = ~d" (rule-pat-num rule-pat)))
                    (when *cexec-trace*
                      (print-next)
                      (flush-all)
                      (let ((*fancy-print* nil)
                            (*print-indent* (+ 4 *print-indent*)))
                        (format t "@[~{~d~^ ~}]" (mapcar #'1+ (rule-pat-pos rule-pat)))
                        (exec-trace-form)
                        (format t " [state ~D-~D] " (rwl-state-depth sub-state) (rwl-state-state sub-state))
                        (term-print-with-sort target-whole)
                        (print-next)
                        (print-axiom-brief (rule-pat-rule rule-pat))
                        (print-next)
                        (print-substitution (rule-pat-subst rule-pat))) ; ***
                      (flush-all))
                    (push sub-state sub-states)))))) ; done apply all rules
          (if sub-states
              (progn
                (when *chaos-verbose*
                  (format t " => ~D (new) states."
                          (length sub-states) ))
                sub-states)
            (progn
              ;; for some unknown reason, no real transitions happened...
              (no-more-transition)
              nil)))))))

;;; RWL-STEP-FORWARD-1
;;; given a rwl-sch-context, execute one step transition for
;;; each `last-siblings' & check if derived terms match to `pattern'.
;;;
(defun rwl-step-forward-1 (sch-context)
  (declare (type rwl-sch-context sch-context)
           (optimize (speed 3) (safety 0)))
  ;; check # of transitions
  (when (>= (rwl-sch-context-trans-so-far sch-context)
            *cexec-limit*)
    (return-from rwl-step-forward-1 (values :max-transitions nil)))
  ;;
  (let ((to-do (rwl-sch-context-last-siblings sch-context))
        (found? nil))
    (when *chaos-verbose*
      (format t "~%-- ~D state(s) to be examined --" (length to-do)))
    ;;
    ;; 1. check for each state if it satisfies the target conditions
    ;;
    (when *chaos-verbose*
      (format t "~&.....condition check for each state.....~%"))
    (loop
      (unless to-do (return nil))       ; done for every state
      (block :continue
        (let ((node (pop to-do)))
          (declare (type rwl-sch-node node))
          ;;
          (when (sch-node-done node)
            ;; already checked 
            (return-from :continue nil))
          ;;
          (let ((state (dag-node-datum node)))
            ;; first prepare applicable rules for the next transition,
            ;; this also marks the state `is-final' iff there are no rules.
            (rwl-state-set-transition-rules state sch-context)
            ;; check state
            (when (and (rwl-sch-context-final-check sch-context)
                       (not (rwl-state-is-final state)))
              (return-from :continue nil)) ; skip this node
            ;;
            (when (rwl-sch-check-conditions node sch-context)
              ;; register answer state
              (push (dag-node-datum node)
                    (rwl-sch-context-answers sch-context))
              ;;
              (when (and (or (= (rwl-state-depth state) 0)
                             *print-every-exec-finding*)
                         (not *rwl-search-no-state-report*))
                (let ((*print-indent* (* 2 (rwl-state-depth state))))
                  (print-next)
                  (format t "** Found [state ~D-~D] " (rwl-state-depth state) (rwl-state-state state))
                  (term-print-with-sort (rwl-state-term state))
                  (print-next)
                  (format t "-- target: ")
                  (term-print (rwl-sch-context-pattern sch-context))
                  (dolist (sub (rwl-state-subst state))
                    (print-subst-if-binding-result state sub sch-context))
                  (print-next)))
              (setf (sch-node-is-solution node) t) ; mark the node as solution
              (incf (rwl-sch-context-sol-found sch-context))
              (setq found? :found)      ; we found at least one solution
              ;; check the # of solutions
              (when (>= (rwl-sch-context-sol-found sch-context)
                        (rwl-sch-context-max-sol sch-context))
                ;; reaches to the # solutions required.
                ;; mesg
                (when (and (= 0 (rwl-state-depth state))
                           (not *rwl-search-no-state-report*))
                  (format t "~%-- found required number of solutions ~D."
                          (rwl-sch-context-max-sol sch-context)))
                (return-from rwl-step-forward-1 (values :max-solutions nil))))))
        )                               ; continue
      )                                 ; end loop
    ;;
    ;; 2. perform the next transitions for each node
    ;;
    (when *chaos-verbose*
      (format t "~%** precompute the next all states......"))
    ;; increment depth
    (incf (rwl-sch-context-cur-depth sch-context))
    ;;
    (let ((next-subs nil))
      (dolist (n (rwl-sch-context-last-siblings sch-context))
        ;; (unless n (break "wow! wow! "))
        (let ((subs (cexec-term-1 n sch-context))
              (nexts nil))
          (dolist (state subs)
            (let ((dag (create-sch-node state)))
              (setf (bdag-parent dag) n)
              (push dag (dag-node-subnodes n))
              (if (rwl-state-loop state)
                  ;; mark `done' if the state is already
                  ;; visited before..
                  (progn
                    (setf (sch-node-done dag) t)
                    (when (rwl-sch-context-if sch-context)
                      (when *cexec-debug*
                        (format t "~%** calling check condition for reporting only."))
                      (rwl-sch-check-conditions dag sch-context))) ; for reporting only
                (push dag nexts))))
          (setq next-subs (nconc next-subs nexts))))
      ;; 
      ;; 3. lastly, set the next states as `last-siblings'
      ;;
      (setf (rwl-sch-context-last-siblings sch-context) next-subs)
      ;;
      (values found? (if next-subs
                         nil
                       :no-more)))))

;;; *********
;;; TOP LEVEL functions
;;; *********
(declaim (inline make-anything-is-ok-term))
(defun make-anything-is-ok-term ()
  (make-variable-term *cosmos* (gensym "Univ")))

(defun rwl-search* (t1 t2 max-result max-depth zero? final?
                    &optional cond
                              pred-pat
                              module
                              bind
                              if)
  (declare (type term t1 t2)
           (type (or null t) zero? final?)
           (optimize (speed 3) (safety 0)))
  (with-in-module (module)
    (unless t2
      (setq t2 (make-anything-is-ok-term)))
    ;; t1 and t2 must be in the same connected component
    (let ((t1-sort (term-sort t1))
          (t2-sort (term-sort t2)))
      (unless (is-in-same-connected-component t1-sort t2-sort *current-sort-order*)
        (with-output-chaos-error ('invalid-sort)
          (format t "Sorts of the source term and the target pattern must be in the same connected component.")
          (format t "~%  Source term : ")
          (term-print-with-sort t1)
          (format t "~&  Target pattern: ")
          (term-print-with-sort t2))))
    (let ((svars (term-variables t1))   ; variables in source
          (pvars (term-variables t2))   ; variables in pattern
          (cvars (if cond               ; variables in suchThat
                     (term-variables cond)
                   nil))
          (predvars (if pred-pat        ; variables in stateEq
                        (term-variables pred-pat)
                      nil))
          (ifvars (if if
                      (term-variables if)
                    nil))
          (allvars nil)
          (.rules-so-far. 0))
      (setq allvars (union svars (union pvars ifvars)))
      ;; check suchThat
      (when cvars
        (unless (subsetp cvars allvars)
          (with-output-chaos-error ('invalid-such-that)
            (format t "`suchThat' introduces new variable(s)."))))
      ;; check variables
      (dolist (v svars)
        (when (memq v pvars)
          (with-output-chaos-error ('subject-var-occus)
            (format t "Variable ")
            (term-print-with-sort v)
            ;; (format t " in subject term occurs in target pattern or coditions..")
            (format t " in subject term occurs in target pattern.")
            (format t "~& subject: ")
            (term-print-with-sort t1)
            (format t "~& pattern: ")
            (term-print-with-sort t2))))
      (dolist (v predvars)
        (when (or (memq v svars)
                  (memq v pvars)
                  (memq v cvars))
          (with-output-chaos-error ('invalid-stateEq)
            (format t "Variable ")
            (term-print-with-sort v)
            (format t " in 'stateEq' occurs in subject term or target pattern or 'suchThat'.."))))
      ;;
      (let ((sch-context (make-rwl-sch-context
                          :module module
                          :term t1
                          :pattern t2
                          :condition cond
                          :zero-trans-allowed zero?
                          :final-check final?
                          :max-sol max-result
                          :max-depth max-depth
                          :state-predicate nil
                          :bind bind
                          :if if
                          :term-hash (alloc-svec term-hash-size)))
            (root nil)
            (res nil)
            (no-more nil)
            (found? nil))
        (flet ((make-state-pred-pat ()
                 (cond (pred-pat
                        (let ((vars (term-variables pred-pat)))
                          (declare (type list vars))
                          (unless (sort= (term-sort pred-pat)
                                         *Bool-sort*)
                            (with-output-chaos-error ('invalid-sort)
                              (format t "state equality must be of a term of sort Bool.")))
                          (unless (= 2 (the fixnum (length vars)))
                            (with-output-chaos-error ('number-of-variables)
                              (format t "state equality pattern must have exactly 2 different variables in it, but ~D given." (length vars))))
                          (unless (sort= (variable-sort (car vars))
                                         (variable-sort (cadr vars)))
                            (with-output-chaos-error ('different-variable-sort)
                              (format t "variables in state equality pattern must be of the same sort.")))
                          (unless (sort<= (term-sort t2) (term-sort (car vars))
                                          *current-sort-order*)
                            (with-output-chaos-error ('invalid-variable-sort)
                              (format t "invalid sort of variable in state equality pattern.")))
                          (cons pred-pat vars)))
                       (t nil))))
          ;;
          ;; initialize search context
          ;;
          (setf (rwl-sch-context-cur-depth sch-context) 0
                (rwl-sch-context-sol-found sch-context) 0
                (rwl-sch-context-trans-so-far sch-context) 0
                root (create-sch-node (make-rwl-state :state 0 :term t1 :depth (1+ .rwl-search-depth.))))
          (setf (rwl-sch-context-root sch-context) root
                (rwl-sch-context-last-siblings sch-context) (list root)
                (rwl-sch-context-answers sch-context) nil)
          ;; state equality predicate
          (setf (rwl-sch-context-state-predicate sch-context) (make-state-pred-pat))
          (let ((.rwl-sch-context. sch-context)
                (.cexec-term-hash. (rwl-sch-context-term-hash sch-context))
                (.rwl-search-depth. (1+ .rwl-search-depth.))
                (.ignore-term-id-limit. t))
            (declare (special .rwl-sch-context. .cexec.term-hash. .ignore-term-id-limit.))
            (push sch-context .rwl-context-stack.)
            ;; the first state is 0
            (set-sch-hashed-term t1 .cexec-term-hash. 0)
            ;;
            ;; do the search
            ;;
            (when *cexec-debug*
              (print sch-context))
            (loop
              (when *chaos-verbose*
                (format t "~%** << level ~D >>" (rwl-sch-context-cur-depth sch-context)))
              (multiple-value-setq (res no-more)
                (rwl-step-forward-1 sch-context))
              (case res
                (:max-transitions (return nil)) ; exit loop
                (:max-solutions
                 (setq found? t)
                 (return nil))          ; exit loop
                (:found
                 (setq found? t))       ; continue..
                (otherwise nil))
              (when no-more
                (when (and (= 0 .rwl-search-depth.)
                           (not *rwl-search-no-state-report*))
                  (format t "~%** No more possible transitions."))
                (return nil))           ; exit if no more ...
              ;; one step deeper
              (when (> (rwl-sch-context-cur-depth sch-context)
                       (rwl-sch-context-max-depth sch-context))
                (unless *rwl-search-no-state-report*
                  (format t "~%-- reached to the specified search depth ~D."
                          (rwl-sch-context-max-depth sch-context)))
                (return-from rwl-search*
                  (if (rwl-sch-context-if sch-context)
                      (if (rwl-sch-context-pr-out? sch-context)
                          :found
                        nil)
                    (if found? :found :max-depth))))) ; end loop
            ;; any solution?
            (cond ((rwl-sch-context-if sch-context)
                   (if (rwl-sch-context-pr-out? sch-context)
                       :found
                     nil))
                  (t (if found? 
                         ;; yes
                         :found
                       ;; no
                       res)))))))))

;;; report-rwl-result
;;;
(defun report-rwl-result (res)
  (case res
    (:max-depth
     ;; (format t "~&-- reached to the max depth.")
     )
    (:no-more
     ;; (format t "~&-- no more solutions.")
     )
    (otherwise
     nil))
  res)

;;; RWL-CONTINUE
;;;
(defun rwl-continue (num-tok)
  (multiple-value-bind (num sym)
      (nat*-to-max-option num-tok)
    (declare (ignore sym))
    (report-rwl-result
     (rwl-continue* num))))

(defun rwl-continue+ (num)
  (report-rwl-result (rwl-continue* num)))

(defun rwl-continue* (num)
  (declare (type fixnum num))
  (unless (and .rwl-sch-context.
               (or (null *current-module*)
                   (eq *current-module*
                       (rwl-sch-context-module .rwl-sch-context.))))
    (with-output-chaos-error ('invalid-context)
      (format t "invalid context...")))
  ;;
  (with-in-module ((rwl-sch-context-module .rwl-sch-context.))
    (setf (rwl-sch-context-max-sol .rwl-sch-context.) num)
    (setf (rwl-sch-context-sol-found .rwl-sch-context.) 0)
    (setf (rwl-sch-context-max-depth .rwl-sch-context.) most-positive-fixnum)
    ;;
    ;; do continue search
    ;;
    (let ((sch-context .rwl-sch-context.)
          (res nil)
          (found? nil))
      (loop
        (setq res (rwl-step-forward-1 sch-context))
        (case res
          ((:max-transitions
            :max-solutions
            :no-more)
           (return nil))                ; exit loop
          (:found
           (setq found? t))
          (otherwise nil))
        ;; one step deeper
        (incf (rwl-sch-context-cur-depth sch-context))) ; end loop
      (if found?
          :found
        res))))

;;; RWL-SEARCH
;;;
(defun rwl-search (&key term
                        pattern
                        (max-result most-positive-fixnum)
                        (max-depth most-positive-fixnum)
                        (zero? nil)
                        (final? nil)
                        (cond nil)
                        (pred nil)
                        (bind nil)
                        ;; the followings are experimental
                        (if nil))
  (let ((module (get-context-module))
        max-r
        max-d)
    (if (integerp max-result)
        (setq max-r max-result)
      (if (term-is-builtin-constant? max-result)
          (setq max-r (term-builtin-value max-result))
        (setq max-r most-positive-fixnum)))
    (if (integerp max-depth)
        (setq max-d max-depth)
      (if (term-is-builtin-constant? max-depth)
          (setq max-d (term-builtin-value max-depth))
        (setq max-d most-positive-fixnum)))
    (when (and if (not (term-is-variable? if)))
      (with-output-chaos-warning ()
        (format t "The `if' part is not a varible of sort BOOL, `if' binding is ignored : ")
        (print-next)
        (term-print if)
        (setq if nil)))
    (when *cexec-normalize*
      (let ((*rewrite-exec-mode* nil)
            (*clean-memo-in-normalize* nil))
        (rewrite* term)))
    ;;
    (when *cexec-debug*
      (format t "~%* CEXEC: ")
      (term-print-with-sort term))
    ;;
    (let ((*clean-memo-in-normalize* nil))
      (report-rwl-result 
       (rwl-search* term pattern max-r max-d zero? final? cond pred module bind if)))))

;;; rwl-check-one-step-reachability : term term -> { t | nil }
;;; working hourse of =>
;;;
(defun rwl-check-one-step-reachability (X Y)
  (declare (type term X Y))
  (let ((*clean-memo-in-normalize* nil)
        (*chaos-quiet* t))
    (report-rwl-result
     (rwl-search* X Y 1 1 t nil nil nil *current-module* nil nil))))

;;; rwl-sch-set-result
;;;
(defun rwl-sch-set-result (raw-res)
  (let ((res nil))
    (if (eq raw-res :found)
        (setq res t)
      (setq res nil))
    (setq $$cexec-term (coerce-to-bool res))))

;;; rwl-cont
;;;
(defun rwl-cont (ast)
  (rwl-continue+ (%continue-num ast)))

;;; for downward compatibility
;;;
(defun nat*-to-max-option (term &optional (infinite most-positive-fixnum))
  (if (term-is-builtin-constant? term)
      (values (term-builtin-value term) "")
    (values infinite (car (method-symbol (term-head term))))))

(defun term-pattern-included-in-cexec (t1 t2 max-depth &optional cond)
  (multiple-value-bind (max sym)
      (nat*-to-max-option max-depth)
    (let ((final? nil)
          (zero? nil))
      (case-equal sym
                  ("!" (setq final? t))
                  ("*" (setq zero? t))
                  (otherwise nil))
      (rwl-search* t1 t2 1 max zero? final? cond nil *current-module*))))

;;; EOF