		Search-engine friendly clone of the ACL2 documentation.

Using-computed-hints

Using-computed-hints-7

Using the stable-under-simplificationp flag

A problem with the example in using-computed-hints-6 is that exactly one simplification occurs between each (effective) firing of the hint. Much more commonly we wish to fire a hint once a subgoal has become stable under simplification.

A classic example of this is when we are dealing with an interpreter for some state machine. We typically do not want the ``step'' function to open up on the symbolic representation of a state until that state has been maximally simplified. We will illustrate with a simple state machine.

Let us start by defining the step function, stp, and the corresponding run function that applies it a given number of times.

(defun stp (s)
  (+ 1 s))

(defun run (s n)
  (if (zp n)
      s
      (run (stp s) (- n 1))))

The step function here is trivial: a state is just a number and the step function increments it. In this example we will not be interested in the theorems we prove but in how we prove them. The formula we will focus on is

(thm (equal (run s 7) xxx))

This is not a theorem, of course. But we want to test our advice on non-theorems because we do not want the advice to work only for proofs that succeed. (In the past, we gave advice about using computed hints and that advice caused the theorem prover to run forever when given formulas that it couldn't prove — but most of the time the system is presented with formulas it cannot prove!)

Furthermore, without some kind of additional rules, the (run s 7) expression in the conjecture above will not expand at all, because ACL2's heuristics do not approve.

In fact, we do not want to take chances that run will be expanded — we want to control its expansion completely. Therefore, disable run.

(in-theory (disable run))

Now, what do we want? (That is always a good question to ask!) We want (run s 7) to expand ``slowly.'' In particular, we want it to expand once, to (run (stp s) 6). Then we want the stp to be expanded and fully simplified before the run expression is expanded again. That is, we want to force the expansion of run whenever the goal is stable under simplification. This is sometimes called ``staged simplification.''

We can achieve staged simplification for any given function symbol by defining the functions shown below and then using a simple computed hint:

(thm (equal (run s 7) xxx)
     :hints ((stage run)))

By inspecting how stage is defined you can see how to extend it, but we explain as we go. To experiment, you can just paste the definitions (and defmacro) below into your ACL2 shell and then try the thm command.

First, define this pair of mutually recursive functions. Find-first-call finds the first call of the function symbol fn in a given term.

(mutual-recursion
 (defun find-first-call (fn term)
 ; Find the first call of fn in term.
  (cond ((variablep term) nil)
        ((fquotep term) nil)
        ((equal (ffn-symb term) fn)
         term)
        (t (find-first-call-lst fn (fargs term)))))
 (defun find-first-call-lst (fn lst)
 ; Find the first call of fn in a list of terms.
  (cond ((endp lst) nil)
        (t (or (find-first-call fn (car lst))
               (find-first-call-lst fn (cdr lst)))))))

We will arrange for the computed hint to generate an :EXPAND hint for the first call of fn, whenever the goal becomes stable under simplification. If no call is found, the hint will do nothing. To make sure the hint will not loop indefinitely (for example, by forcing fn to expand only to have the rewriter ``fold'' it back up again), we will provide the hint with a bound that stops it after some number of iterations. Here is the basic function that creates the expand hint and replaces itself to count down.

(defun stage1 (fn max clause flg)
; If the clause is stable under simplification and there is a call of
; fn in it, expand it.  But don't do it more than max times.
 (let ((temp (and flg
                  (find-first-call-lst fn clause))))
   (if temp
       (if (zp max)
           (cw "~%~%HINT PROBLEM:  The maximum repetition count of ~
                your STAGE hint has been reached without eliminating ~
                all of the calls of ~x0.  You could supply a larger ~
                count with the optional second argument to STAGE ~
                (which defaults to 100).  But think about what is ~
                happening! Is each stage permanently eliminating a ~
                call of ~x0?~%~%"
               fn)
         `(:computed-hint-replacement
            ((stage1 ',fn ,(- max 1)
                     clause
                     stable-under-simplificationp))
           :expand (,temp)))
     nil)))

Suppose that when stage1 is called, fn is the function we want to expand, max is the maximum number of iterations of this expansion, clause is the current goal clause, and flg is the value of the stable-under-simplificationp flag. Then if clause is stable and we can find a call of fn in it, we ask whether max is exhausted. If so, we print an ``error message'' to the comment window with cw and return nil (the value of cw). That nil means the hint does nothing. But if max is not yet exhausted, we return a new hint. As you can see above, the hint replaces itself with another stage1 hint with the same fn and a decremented max to be applied to the new clause and the then-current value of stable-under-simplificationp. The hint also contains an :expand directive for the call of fn found.

Thus, if the computed hint was:

(stage1 'run 5 clause stable-under-simplificationp)

and (run s 7) occurs in the clause, then it will generate

(:computed-hint-replacement
  ((stage1 'run 4 clause stable-under-simplificationp))
 :expand ((run s 7)))

which will in turn replace the old stage1 hint with the new one and will apply :expand ((run s 7)) to the current goal.

We can make this more convenient by defining the macro:

(defmacro stage (fn &optional (max '100))
 `(stage1 ',fn ,max clause stable-under-simplificationp))

Note that the macro allows us to either provide the maximum bound or let it default to 100.

Henceforth, we can type

(thm (equal (run s 7) xxx)
     :hints ((stage run)))

to stage the opening of run up to 100 times, or we can write

(thm (equal (run s 7) xxx)
     :hints ((stage run 5)))

to stage it only 5 times. In the latter example, the system will print an ``error message'' after the fifth expansion.

Note that if we executed

(set-default-hints '((stage run)))

then we could attack all theorems (involving run) with staged simplification (up to bound 100), without typing an explicit hint.

(thm (equal (run s 7) xxx))

Using techniques similar to those above we have implemented ``priority phased simplification'' and provided it as a book. See community book books/misc/priorities.lisp. This is an idea suggested by Pete Manolios, by which priorities may be assigned to rules and then the simplifier simplifies each subgoal maximally under the rules of a given priority before enabling the rules of the next priority level. The book above documents both how we implement it with computed hints and how to use it.

Here is another example of using the stable-under-simplificationp flag to delay certain actions. It defines a default hint, see default-hints, which will enable non-linear-arithmetic on precisely those goals which are stable-under-simplificationp. It also uses the HISTORY and PSPV variables to determine when toggling non-linear-arithmetic is appropriate. These variables are documented only in the source code. If you start using these variables extensively, please contact the developers of ACL2 or Robert Krug (rkrug@cs.utexas.edu) and let us know how we can help.

(defun nonlinearp-default-hint (stable-under-simplificationp hist pspv)
  (cond (stable-under-simplificationp
         (if (not (access rewrite-constant
                          (access prove-spec-var pspv :rewrite-constant)
                          :nonlinearp))
             '(:computed-hint-replacement t
               :nonlinearp t)
           nil))
        ((access rewrite-constant
                 (access prove-spec-var pspv :rewrite-constant)
                 :nonlinearp)
         (if (not (equal (caar hist) 'SETTLED-DOWN-CLAUSE))
             '(:computed-hint-replacement t
               :nonlinearp nil)
           nil))
        (t
         nil)))