		Search-engine friendly clone of the ACL2 documentation.

Type-reasoning

Set-dwp

Affect the effort made in type-reasoning

This is a relatively advanced event that affects the type-reasoning heuristics. (The name “dwp” stands for “double-whammy property” because the effect pertains to making a second attempt.) The default behavior is obtained with (set-dwp nil), but type reasoning makes an extra effort after evaluation of (set-dwp t).

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. It is local to the book or encapsulate form in which it occurs; see set-dwp! for a corresponding non-local event.

General Form:
(set-dwp val)

where val is arbitrary but is typically t or nil, since every non-nil value is treated the same as t.

The following example, from Eric Smith, proves after evaluating (set-dwp t) but otherwise fails.

(thm
 (implies (and (<= 0 (* 2 k)) ; extra hyp ;
               (unsigned-byte-p 4 k)
               (integerp x)
               (< x (+ 4 (* 2 k))))
          (<= x (+ 3 (* 2 k))))
 :hints (("Goal" :in-theory (disable unsigned-byte-p))))

So why not always evaluate (set-dwp t) at the beginning of an ACL2 session? Such a change added 3.9% to the certification of the ACL2 community books, and at least one book took almost twice as long to certify. That isn't a huge penalty, but on the other hand it seems likely that (set-dwp t) is helpful only in rare instances.

To get the current value of dwp, evaluate (get-dwp nil (w state)).