Major Section: NOTE-2-7

An improvement in the linear arithmetic heuristics has been provided
by Robert Krug. For information about this change, search for the
comment in `add-linear-lemma`

(file `rewrite.lisp`

) that begins
as follows.

; Previous to Version_2.7, we just went ahead and used the result ofThanks, Robert! Also thanks to Eric Smith for providing a motivating example.

The non-linear-arithmetic addition (see non-linear-arithmetic) led to several small changes in the linear-arithmetic decision procedure (see linear-arithmetic). Two of these changes could affect existing proofs.

First, when we are setting up the initial arithmetic database (which we call the ``pot-lst''), we have always scanned it to see if there were any pairs of inequalities from which we could derive a previously unknown equality. In some cases we added this equality to the clause and in others we used it to rewrite the clause, substituting one side of the equality for the other throughout the clause. Previously, the heuristics that we used to determine whether we performed the substitution differed from those used in several other places in the code. This has now been regularized, and similar heuristics are now used throughout the code.

The second change to the linear-arithmetic decision procedure is that we now explicitly add inequalities derived from type reasoning to the pot-lst. Previously, we performed cancellations against these inequalities without adding them to the pot-lst. This change results in there being more inequalities in the pot-lst than before, and so more chances for there to be a pair of inequalities from which an equality can be derived. In effect, certain simple consequences of the current goal (see type-set) may now be added as hypotheses of the goal or used to peform equality substitutions.

A slight improvement has been made to the way certain rewrite rules are
stored. It was already the case that a rewrite rule rule whose conclusion
`C`

is not a call of a known equivalence relation (or `eq`

, `eql`

,
or `=`

) is stored as `(iff C t)`

, except that if ACL2 can determine
(using its `type-set`

mechanism) that `C`

is Boolean, then the rule is
stored as `(equal C t)`

. The iprovement is that if `C`

and `C'`

are
Boolean, then a rule stated as `(iff C C')`

is stored as `(equal C C')`

.
Thanks to Pete Manolios for providing an example that led us to consider this
improvement.

The heuristic use of equalities (fertilization) has been modified.
Previously, ACL2 would sometimes substitute using an equality but keep the
equality, and then undo the substitution by using the equality again. Now,
when ACL2 keeps an equality after using it, it puts the equality inside a
call of `hide`

. Descendents of that goal that are unchanged by
simplification will have this call of `hide`

removed so that the equality
can once again contribute to the proof. This change can cause some proofs to
succeed that otherwise would fail. In the unlikely event that a proof fails
that formerly succeeded, the following hint on "Goal" may fix the problem
(see hints):

:expand ((:free (x) (hide x)))

We have refined the heuristics employed when an `IF`

form is assumed true
or false. Our previous attempt (see note-2-6-proofs for the original
announcement) was not as general as we had believed. We have also improved
some low-level code responsible for rewriting `IF`

expressions. In
earlier versions of ACL2, it was possible to have the truth or falsity
of an `IF`

expression explicitly recorded in the type-alist, and yet
not use this information during rewriting. This problem has been corrected.
Thanks to Robert Krug for noticing this problem and implementing the fix.

We have sped up the rewriter in some cases where there are large collections
of mutually-recursive functions (see mutual-recursion). (Implementation
notes: technically, we have modified the way function `being-openedp`

operates on the `fnstack`

, and we have modified
`*current-acl2-world-key-ordering*`

as described in the essay above its
definition.)

Forward-chaining is now done in the preprocessing phase of proof
attempts (see the discussion of `:DO-NOT`

-- see hints). This is part
of a technical change, made in support of translation of type declarations to
guards (see note-2-7-guards). Previously, whenever ACL2 checked for
built-in-clauses, it then looked for a contradiction using
`type-set`

reasoning if it did not find a suitable built-in clause. The
change is to perform forward-chaining in such cases (i.e., when a built-in
clause is not found).

A couple of changes have been made in the generation of goals for
forcing-rounds. Thanks to Eric Smith for bringing issues to our
attention that led to these changes. For one, guards are no longer
relevant in such goal generation. Formerly, the addition of a guard could
make a proof fail that otherwise succeeded. Secondly, contextual information
is now always kept when it involves a constrained constant, i.e., a zero-ary
function introduced in the signature of an `encapsulate`

.