Major Section: NOTE-2-8
ACL2 now prevents certain rewriting loops; see rewrite-stack-limit.
During the computation of constraints for functional instantiation,
(prog2$ term1 term2) and (the type term2) are now treated as
term2.
A change has been made in heuristics for controlling rewriting during proofs by induction. Formerly, during induction proofs, ACL2 suppressed rewriting of certain ``induction hypothesis'' terms, and forced expansion of certain ``induction conclusion'' terms, until rewriting had stabilized. This meddling with the rewriter is still turned off when rewriting has stabilized, but it is now turned off earlier once an ancestor has been through the rewriter and the current goal is free of ``induction conclusion'' terms. Thanks to Dave Greve and Matt Wilding for providing an example and associated analysis that led us to look for a heuristic modification.
A change has been made in the heuristics for handling certain ``weak''
compound-recognizer rules when building contexts. Those who want to dig
deeply into this change are welcome to look at the code following the call of
most-recent-enabled-recog-tuple in the code for function
assume-true-false in the ACL2 sources.
The handling of free variables in a hypothesis of a rewrite rule
(see free-variables) has been improved in the case that the hypothesis is of
the form (equiv x y), where equiv is a known equivalence relation
(see equivalence). Previously, if the rewriter was attempting to rewrite
the hypothesis (equiv x y) of a rewrite rule, in a context where x'
is an instance of x, then the rewriter could fail to notice a term
(equiv x' y') true in the current context where y' is an instance of
y, in the case that x' precedes y' in the term-order. This
has been remedied. This improvement applies regardless of whether x,
y, or (we believe) both are already fully instantiated in the present
context. Thanks to Joe Hendrix for bringing up an example and to Vernon
Austel for providing another, simple example.
A very minor change has been made to the rewriter in the case that an
equality appears on the left-hand side of a :rewrite rule.
Formerly, when such an equality (equal x y) was commuted to
(equal y x) in order for the rule to match the current term, then all
equalities on the instantiated right-hand side of the rule were commuted,
except for those occurring inside another equality. The instantiated
right-hand side is no longer modified. It seems very unlikely that this
change will cause proofs to fail, though we cannot completely rule out that
possibility.
We have modified how the ACL2 simplifier handles the application of a defined
function symbol to constant arguments in certain cases, which we now
describe. As before, ACL2 attempts to simplify such a function application
by evaluation, provided the :executable-counterpart of the function
is enabled. And as before, if that evaluation fails due to a subroutine call
of a constrained function (introduced by encapsulate), ACL2 may wrap a
call of hide around this function application. (See hide.) But now,
ACL2 attempts to apply definitions and rewrite rules in the case that this
evaluation fails, and only if the resulting term is unchanged does ACL2 wrap
hide around this function application. Thanks to Matt Wilding for
bringing up the idea of this modification.
The generation of "Goal" for recursive (and mutually-recursive) definitions now uses the subsumption/replacement limitation (default 500). See case-split-limitations.
Default hints now apply to hints given in definitions, not just theorems. See default-hints.
Thanks to Robert Krug for implementing the following two improvements
involving linear arithmetic reasoning: linear arithmetic now uses the
conclusions of forward-chaining rules, and type-set now uses a
small amount of linear reasoning when deciding inequalities.