DEALING-WITH-TAU-PROBLEMS

Major Section:  INTRODUCTION-TO-THE-TAU-SYSTEM

For background on the tau system, see introduction-to-the-tau-system. The two most common problems caused by the tau system have to do with the system's interaction with ``legacy'' proof scripts. Such scripts may suffer because they were not designed to exploit tau reasoning and which may configure the tau database in quite incomplete and arbitrary ways. The two most common problems we have seen are (a) significant slow downs in a few proofs and (b) failed proof attempts due to hints being misapplied because the tau system caused subgoals to be renumbered.

We discuss the rather limited means of dealing with these problems here. In future-work-related-to-the-tau-system we list some major inadequacies of the tau system.

If the tau system contributes to a proof, the rune (:executable-counterpart tau-system) will be listed among the Rules in the Summary. However, merely by being attempted the tau system can slow down proofs in which it makes no contribution.

The most brutal and fool-proof way to isolate a proof from the tau system is to disable the entire system. This can be done globally by

(in-theory (disable (tau-system)))  ; (:executable-counterpart tau-system)

...
:hints (("...subgoal id..." :in-theory (disable (tau-system))))

Dealing with Slowdowns

The time-tracker utility was added to allow users to investigate whether excessive amounts of time are being spent in a given function. It was then used to annotate the code for the tau system as described in time-tracker-tau. The result is that if ``excessive'' time is spent in tau reasoning, messages to that effect will be printed to the proof log. The question is: aside from disabling the tau system how can the proof be sped up?

There are two common causes of slowdown in the tau system. The first stems from the system's use of :executable-counterparts to determine whether a constant has a given tau. Recall that a tau is a conjunction of monadic predicates. To determine whether some constant satisfies the tau, the predicates are executed. If you have a hard-to-compute predicate this can be very slow. The most typical such predicates in ACL2 applications are those that check invariants, e.g., that recognize ``good states'' or ``well-formed data.'' These are often written inefficiently because they are intended only for used in theorems and, before the tau system was added, they may have never been applied to constants. The most common constants tau predicates are applied to are 0, T, and NIL, although different models may stress other constants. To understand why NIL for example is frequently tested, if the test of an IF-expression is computed to have tau s then the next question we ask is ``does nil satisfy s?''

You may determine whether the tau system is spending time executing tau predicates by observing the rewriter -- see dmr -- or by interrupting the system and getting a backtrace (see set-debugger-enable).

If excessive time is being spent in a tau predicate, a draconian solution is to disable the :executable-counterpart of that predicate, for example in either of these equivalent ways. The tau system does not execute disabled :executable-counterparts.

(in-theory (disable (:executable-counterpart foo)))
(in-theory (disable (foo)))

Disabling the executable counterpart of expensive tau predicates will weaken the tau system, probably only negligibly, because it can no longer run the predicates to determine whether they admits given constants.

A more sophisticated solution is to make the tau system record values of the :logic-mode function in question, so that the system will look up the necessary values rather than running the function every time the question arises. It will look up recorded values whether the executable counterpart of the tau predicate is enabled or disabled. Here is an example of a lemma that can provide such a solution. See the discussion of the Eval form of :tau-system rules.

(defthm lemma
  (and (foo 0)
       (foo 17)
       (foo t)
       (not (foo '(a b c))))
  :rule-classes :tau-system)

It might be difficult to determine which constants are being repeatedly tested, although tracing (trace$) suspected tau predicates will show what they are being called on.

At the moment there are no better user-level tools to discover this. However, some users may wish to consider the following hack: In the ACL2 source file tau.lisp, immediately after the definition of the system function ev-fncall-w-tau-recog, there is a comment which contains some raw Lisp code that can be used to investigate whether tau's use of evaluation on constants is causing a problem and to determine which constants are involved.

The second main cause of slowdowns by the tau system is that the system contains ``too many'' conjunctive rules (see the Conjunctive form in tau-system). Unfortunately, we have no tools for either identifying the problem or addressing it! That said, let us tell you what we do know!

Conjunctive rules are used to ``complete'' each tau as it is built. Referring to the weekdayp example in tau-system, if a tau is constructed that recognizes weekdays but not MON, TUE, THU, or FRI, it is completed by adding that the tau recognizes (only) WED. This means that when we construct a tau we scan all known conjunctive rules and see whether all but one of the literals of any conjunctive rule are present. This can be expensive. To mitigate this expense, the tau system caches the computation on a per proof basis (the cache is cleared after every proof).

To learn what conjunctive rules there are in your system, evaluate

(assoc 'tau-conjunctive-rules (tau-database (w state)))

Dealing with Misapplied Hints

The second common problem caused by the tau system in legacy proof scripts is that it can cause subgoals to be renumbered and thus cause hints to be missed. The only ways to address this problem is either to disable the tau system (locally or globally by disabling (:executable-counterpart tau-system)) or change the legacy hints to use the new subgoal names.