Avoiding infinite loops in the ACL2 rewriter
                                 Matt Kaufmann
                             ACL2 Seminar 1/15/03

Here is an example using ACL2 Version 2.8 (development version).

ACL2 !>(defthm app-assoc-1
         (equal (append (append x y) z)
                (append x y z)))
....
Time:  0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)
 APP-ASSOC-1
ACL2 !>(defthm app-assoc-2
         (equal (append x y z)
                (append (append x y) z)))
....
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 APP-ASSOC-2
ACL2 !>(thm (equal (append a b c) xxx))


HARD ACL2 ERROR in PREPROCESS:  The call depth limit of 1000 has been
exceeded in the ACL2 preprocessor (a sort of rewriter).  There is probably
a loop caused by some set of enabled simple rules.  To see why the
limit was exceeded, execute
  :brr t
and next retry the proof with :hints
  :do-not '(preprocess)
and then execute the form (cw-gstack).  See :DOC rewrite-stack-limit.



ACL2 Error in TOP-LEVEL:  Evaluation aborted.  You *MAY* be able to
see a trace of calls leading up to this  violation by executing (wet
<form>), where <form> is the form you submitted to the ACL2 loop. 
See :DOC wet for how to get an error backtrace.

ACL2 !>:brr t
The monitored runes are:
NIL
 T
ACL2 !>:set-rewrite-stack-limit 30
 20
ACL2 !>(thm (equal (append a b c) xxx)
            :hints (("Goal" :do-not '(preprocess))))

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]


HARD ACL2 ERROR in REWRITE:  The call depth limit of 30 has been exceeded
in the ACL2 rewriter.  There is probably a loop caused by some set
of enabled rules.  To see why the limit was exceeded, execute the form
(cw-gstack).  See :DOC rewrite-stack-limit.



ACL2 Error in TOP-LEVEL:  Evaluation aborted.  You *MAY* be able to
see a trace of calls leading up to this  violation by executing (wet
<form>), where <form> is the form you submitted to the ACL2 loop. 
See :DOC wet for how to get an error backtrace.

ACL2 !>(cw-gstack) ; note 4, 6, 8, 10
1. Simplifying the clause
     ((EQUAL (BINARY-APPEND A (BINARY-APPEND B C))
             XXX))
2. Rewriting (to simplify) the atom of the first literal,
     (EQUAL (BINARY-APPEND A (BINARY-APPEND B C))
            XXX),
3. Rewriting (to simplify) the first argument,
     (BINARY-APPEND A (BINARY-APPEND B C)),
4. Attempting to apply (:REWRITE APP-ASSOC-2) to
     (BINARY-APPEND A (BINARY-APPEND B C))
5. Rewriting (to simplify) the rhs of the conclusion,
     (BINARY-APPEND (BINARY-APPEND X Y) Z),
   under the substitution
     Z : C
     Y : B
     X : A
6. Attempting to apply (:REWRITE APP-ASSOC-1) to
     (BINARY-APPEND (BINARY-APPEND A B) C)
7. Rewriting (to simplify) the rhs of the conclusion,
     (BINARY-APPEND X (BINARY-APPEND Y Z)),
   under the substitution
     Z : C
     Y : B
     X : A
8. Attempting to apply (:REWRITE APP-ASSOC-2) to
     (BINARY-APPEND A (BINARY-APPEND B C))
9. Rewriting (to simplify) the rhs of the conclusion,
     (BINARY-APPEND (BINARY-APPEND X Y) Z),
   under the substitution
     Z : C
     Y : B
     X : A
10. Attempting to apply (:REWRITE APP-ASSOC-1) to
     (BINARY-APPEND (BINARY-APPEND A B) C)
....

31. Rewriting (to simplify) the first argument,
     X,   under the substitution
     Y : B
     X : A
NIL
ACL2 !>
.................... Notes on the default (1000) ....................

I collected statistics on the regression suite by uncommenting this new line at
the bottom of acl2.lisp, before compiling.

; (push :acl2-rewrite-meter *features*)

The regression suite then produced files *.rstats which were collected into a
single file (now in logs/rewrite-depth-stats.lisp under the v2-8 sources).
This was then analyzed with a function collect-rstats, creating file
logs/rewrite-depth-stats.out, which shows that the maximum depth required was
186.  However, a proof at AMD involving a hypothesis of (member x '(255 254 253
... 2 1 0)) has required a value of 774.  A stack limit of 1000 seems safe for
avoiding stack overflows.  The example with the :do-not hint in :doc
rewrite-stack-limit caused a stack overflow in GCL with
(set-rewrite-stack-limit 4350) but not 4300, or even 15000 without the :do-not.