; Illustration of dynamic monitoring of rules

; Load the commands in the following distributed book (file).
(ld "misc/getprop.lisp" :dir :system)

:ubt! timed-fnd-is-no-duplicatesp

; Goes "out to lunch" (here, without a hint); must interrupt.
(defthm timed-fnd-is-no-duplicatesp ; FAILS!! - interrupt
  (equal (mv-nth 1 (timed-fnd lst state))
         (no-duplicatesp lst)))

; Try this, and then try again.
(accumulated-persistence t)

; Interrupt this:
(defthm timed-fnd-is-no-duplicatesp ; FAILS!! - interrupt
  (equal (mv-nth 1 (timed-fnd lst state))
         (no-duplicatesp lst)))

(show-accumulated-persistence) ; not helpful; see advice

(show-accumulated-persistence
 :frames-a) ; helpful, but ignore

:dmr-start ; "DMR": "Dynamic Monitoring of Rewrites"

; Hit control-t 1 after this starts.  It will be obvious what
; will probably help!
(defthm timed-fnd-is-no-duplicatesp ; Hit control-t 1
  (equal (mv-nth 1 (timed-fnd lst state))
         (no-duplicatesp lst)))

:dmr-stop

(defthm timed-fnd-is-no-duplicatesp ; now succeeds
  (equal (mv-nth 1 (timed-fnd lst state))
         (no-duplicatesp lst))
  :hints (("Goal"
           :in-theory
           (disable print-rational-as-decimal))))

; Stack of rules we could disable, and whether such disabling
; results in a successful proof of the above theorem:

; No:  TIMED-FND
; Yes: PRINT-TIMER
; Yes: PRINT-RATIONAL-AS-DECIMAL
; Yes: PRINC$
; Yes (but slow): EXPLODE-ATOM
; Yes (but slow): EXPLODE-NONNEGATIVE-INTEGER
; Yes (but very slow): PRINT-BASE-P