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
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)or locally with a subgoal specific hint:
... :hints (("...subgoal id..." :in-theory (disable (tau-system))))Conducting a proof with and without the participation of the tau system can help you determine whether tau reasoning is helping or hurting.
Dealing with Slowdowns
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
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
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
(in-theory (disable (:executable-counterpart foo))) (in-theory (disable (foo)))In either case above, you may prefer to provide local
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
(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
tau.lisp, immediately after the definition of the system
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
The second main cause of slowdowns by the tau system is that the system contains
``too many'' conjunctive rules (see the Conjunctive form in
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
FRI, it is completed by adding that the tau recognizes (only)
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
To learn what conjunctive rules there are in your system, evaluate
(assoc 'tau-conjunctive-rules (tau-database (w state)))Perhaps by sending the implementors that list, we can think of ways to index the conjunctive rules to save time.
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.