; ACL2 Patch Version 3.2-4. See source file axioms.lisp for authorship and
; licensing information.
; Copyright (C) 2007 University of Texas at Austin
; Table of Contents:
;;; PATCH INSTALLATION
;;; PATCH USAGE
;;; WHAT THIS PATCH FILE FIXES
;;; CODE
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; PATCH INSTALLATION
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Just once, certify this book:
; (certify-book "patch-3.2-4" 0 t :ttags (:patch))
; For an alternate approach, see the NOTE below.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; PATCH USAGE
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; After the above certify-book, you can include this patch as follows:
; (include-book "patch-3.2-4" :ttags (:patch))
; NOTE: This include-book generally must be undone (with :u or :ubt) in order
; to certify books. If you want to avoid that need to undo, then consider
; using the "-raw.lisp" version instead.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; WHAT THIS PATCH FILE FIXES
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; We quote below from what will be :DOC NOTE-3-3.
#||
(OpenMCL and multi-threaded SBCL only) Fixed a soundness bug in the
evaluation of mbe forms in the presence of Lisp feature
:acl2-mv-as-values. Thanks to Sol Swords for reporting this problem and
sending a simple proof of nil (which can be found in a comment in the
ACL2 sources, in (deflabel note-3-3 ...)).
Fixed a bug in evaluation of calls of with-prover-time-limit.
Fixed bugs in :pl (which are similarly present in the proof-checker's sr
(show-rewrites) command. The first bug was evident from the following
forms sent by Robert Krug, which caused an error.
(include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)
:pl (mod (+ 1 x) n)
The second bug was due to a failure to take note of which rules are
disabled, and could be seen by executing the following (very slow!).
(defstub modulus () t)
(include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)
:pl (mod (+ x y) (modulus))
Enhanced accumulated-persistence to break down results by useful vs.
useless rule applications. In particular, this provides information
about which rules were ever applied successfully, as requested by Bill
Young.
Fixed a bug that was causing a :clause-processor hint to fire on a
subgoal of the goal to which it was attached, when the original
application didn't change the clause. Thanks to Dave Greve for
pointing out this bug and providing a useful example.
Added coverage of :meta rules to the accumulated-persistence statistics.
||#
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; CODE
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Preliminary stuff
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
(defttag :patch)
(progn!
(state-global-let*
((temp-touchable-vars t set-temp-touchable-vars))
(progn!
(f-put-global
'built-in-program-mode-fns
(add-to-set-eq
'pc-relieve-hyp
; Put functions into this list that should not be put into :logic mode, because
; we want to execute their raw Lisp code. There is also a mechanism in
; oneify-cltl-code that prevents the *1* body of such a function from being
; called (e.g. in safe-mode, during macroexpansion), provided (important!) that
; the function is in this list at the time it is admitted.
(f-get-global 'built-in-program-mode-fns state))
state)
; (redef!)
(SET-LD-REDEFINITION-ACTION '(:WARN! . :OVERWRITE)
STATE)
(PROGRAM)
(SET-STATE-OK T))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Fix for soundness bug related to mbe and mv
;;; and for bug in evaluation of calls of with-prover-time-limit
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(progn!
(set-raw-mode t)
(defun-one-output oneify (x w)
; Keep this function in sync with translate11. Errors have generally
; been removed, since we know they can't occur.
(cond
((or (atom x) (eq (car x) 'quote))
(cond ((keywordp x)
(kwote x))
((symbolp x)
; At one time we returned (defined-constant x w) here in the case that
; (legal-constantp1 x). But when the constant is replaced by its value, we can
; wind up with slow array accesses, since the constant and the written-out
; value need not be EQ.
x)
((atom x) (kwote x))
(t x)))
((not (symbolp (car x)))
(oneify
(list* 'let (listlis (cadr (car x))
(cdr x))
(cddr (car x)))
w))
((or (member-eq (car x) *oneify-primitives*)
; Note that safe-mode for make-event will require addition of the following two
; lines:
; (member-eq (car x) *primitive-event-macros*)
; (assoc-eq (car x) *super-defun-wart-table*)
(member-eq (car x) *macros-for-nonexpansion-in-raw-lisp*))
(let ((args (oneify-lst (cdr x) w)))
(cons (car x) args)))
((eq (car x) 'mv-let)
(let ((value-form (oneify (caddr x) w))
(body-form (oneify (car (last x)) w)))
`(mv-let ,(cadr x)
,value-form
; We leave the DECLAREs in place so that the compiler can see the
; IGNOREs at least.
,@(butlast (cdddr x) 1)
,body-form)))
#| Feb 8, 1995. Once upon a time we had the following code here:
((eq (car x) 'the)
(let ((value-form (oneify (caddr x) w)))
`(the ,(cadr x) ,value-form)))
But that led to garbage for a user defined function like
(defun foo (x) (declare (xargs :verify-guards nil)) (the integer x))
because (foo 3) = 3 but (foo t) would cause a hard error. We now
just macroexpand the just like we would any other macro. We are not
sure why we ever thought we could handle it any other way.
|#
((eq (car x) 'translate-and-test)
(oneify (caddr x) w))
((eq (car x) 'with-local-stobj)
(mv-let (erp st mv-let-form creator)
(parse-with-local-stobj (cdr x))
(declare (ignore erp)) ; should be nil
(mv-let-for-with-local-stobj mv-let-form st creator w)))
((getprop (car x) 'macro-body nil 'current-acl2-world w)
(oneify (macroexpand1! x) w))
((eq (car x) 'let)
(let ((value-forms
(oneify-lst (strip-cadrs (cadr x)) w))
(body-form (oneify (car (last x)) w)))
`(let ,(listlis (strip-cars (cadr x))
value-forms)
,@(butlast (cddr x) 1)
,body-form)))
((eq (car x) 'must-be-equal) ; (must-be-equal logic exec)
(oneify (cadr x) w))
((eq (car x) 'prog2$)
; We need to avoid dropping values in the multiple-value case when
; #+acl2-mv-as-values. But this seems like a reasonable step to take in
; general.
(let ((args (oneify-lst (cdr x) w)))
(cons 'progn args)))
((eq (car x) 'time$)
(list 'time (oneify (cadr x) w)))
((eq (car x) 'with-prover-time-limit)
(list (car x) (oneify (cadr x) w) (oneify (caddr x) w)))
(t
(let ((arg-forms (oneify-lst (cdr x) w)))
(cons (*1*-symbol (car x)) arg-forms)))))
)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Fix for :clause-processor hint bug
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defun all-runes-in-ttree (ttree ans)
; Ttree is any ttree produced by this system. We sweep it collecting into ans
; every rune in it.
(cond
((null ttree) ans)
((symbolp (caar ttree))
(all-runes-in-ttree
(cdr ttree)
(let ((val (cdar ttree)))
; Val is the value of the tag. Below we enumerate all possible tags. For each
; we document the shape of val and then process it for runes.
(case
(caar ttree)
(lemma ;;; Shape: rune
(add-to-set-equal val ans))
(:by ;;; Shape: (lmi-lst thm-cl-set constraint-cl k)
;;(all-runes-in-lmi-lst (car val) wrld ans)
; As of this writing, there aren't any runes in an lmi list that are
; being treated as runes. Imagine proving a lemma that is then
; supplied in a :use hint. It shouldn't matter, from the point of
; view of tracking RUNES, whether that lemma created a rewrite rule that
; is currently disabled or whether that lemma has :rule-classes nil.
ans)
(:bye ;;; Shape: (name . cl), where name is a
;;; "new" name, not the name of something used.
ans)
(:use ;;; Shape: ((lmi-lst (hyp1 ...) cl k) . n)
;;(all-runes-in-lmi-lst (car (car val)) wrld ans)
; See comment for the :by case above.
ans)
(:cases ;;; Shape: ((term1 ... termn) . clauses)
ans)
(preprocess-ttree ;;; Shape: ttree
(all-runes-in-ttree val ans))
(assumption ;;; Shape: term
ans)
(pt ;;; Shape: parent tree - just numbers
ans)
(fc-derivation ;;; Shape: fc-deriviation record
(add-to-set-equal (access fc-derivation val :rune)
(all-runes-in-ttree (access fc-derivation val :ttree)
ans)))
(find-equational-poly ;;; Shape: (poly1 . poly2)
(all-runes-in-ttree (access poly (car val) :ttree)
(all-runes-in-ttree (access poly (cdr val) :ttree)
ans)))
(variables ;;; Shape: var-lst
ans)
(elim-sequence ;;; Shape: ((rune rhs lhs alist
;;; restricted-vars
;;; var-to-runes-alist
;;; ttree) ...)
(all-runes-in-elim-sequence val ans))
((literal ;;; Shape: term
hyp-phrase ;;; tilde-@ phrase
equiv ;;; equiv relation
bullet ;;; term
target ;;; term
cross-fert-flg ;;; boolean flg
delete-lit-flg ;;; boolean flg
clause-id) ;;; clause-id
ans)
((terms ;;; Shape: list of terms
restricted-vars) ;;; list of vars
ans)
(var-to-runes-alist ;;; Shape: (...(var . (rune1 ...))...)
(all-runes-in-var-to-runes-alist val ans))
(ts-ttree ;;; Shape: ttree
(all-runes-in-ttree val ans))
((irrelevant-lits ;;; Shape: clause
clause) ;;; clause
ans)
(hidden-clause ;;; Shape: t
ans)
(abort-cause ;;; Shape: symbol
ans)
(bddnote ;;; Shape: bddnote
; A bddnote has a ttree in it. However, whenever a bddnote is put into a given
; ttree, the ttree from that bddnote is also added to the same given ttree.
; So, we don't really think of a bddnote as containing a "ttree" per se, but
; rather, a sort of data structure that is isomorphic to a ttree.
ans)
(case-limit ;;; Shape: t
ans)
(sr-limit ;;; Shape: t
ans)
(:clause-processor
ans)
(otherwise (er hard 'all-runes-in-ttree
"This function must know every possible tag so that it ~
can recover the runes used in a ttree. The unknown ~
tag ~x0, whose value is ~x1, has just been encountered."
(caar ttree)
(cdar ttree)))))))
(t (all-runes-in-ttree (cdr ttree)
(all-runes-in-ttree (car ttree) ans)))))
(defun no-op-histp (hist)
; We say a history, hist, is a "no-op history" if it is empty or its most
; recent entry is a to-be-hidden preprocess-clause or apply-top-hints-clause
; (possibly followed by a settled-down-clause).
(or (null hist)
(and hist
(member-eq (access history-entry (car hist) :processor)
'(apply-top-hints-clause preprocess-clause))
(tag-tree-occur 'hidden-clause
t
(access history-entry (car hist) :ttree)))
(and hist
(eq (access history-entry (car hist) :processor)
'settled-down-clause)
(cdr hist)
(member-eq (access history-entry (cadr hist) :processor)
'(apply-top-hints-clause preprocess-clause))
(tag-tree-occur 'hidden-clause
t
(access history-entry (cadr hist) :ttree)))))
(defun preprocess-clause (cl hist pspv wrld state)
; This is the first "real" clause processor (after a little remembered
; apply-top-hints-clause) in the waterfall. Its arguments and
; values are the standard ones. We expand abbreviations and clausify
; the clause cl. For mainly historic reasons, expand-abbreviations
; and clausify-input operate on terms. Thus, our first move is to
; convert cl into a term.
(let ((rcnst (access prove-spec-var pspv :rewrite-constant)))
(mv-let
(built-in-clausep ttree)
(cond
((or (eq (car (car hist)) 'simplify-clause)
(eq (car (car hist)) 'settled-down-clause))
; If the hist shows that cl has just come from simplification, there is no
; need to check that it is built in, because the simplifier does that.
(mv nil nil))
(t
(built-in-clausep cl
(access rewrite-constant
rcnst
:current-enabled-structure)
(access rewrite-constant
rcnst
:oncep-override)
wrld
state)))
; Ttree is known to be 'assumption free.
(cond
(built-in-clausep
(mv 'hit nil ttree pspv))
(t
; Here is where we expand the "original" IMPLIES in the conclusion but
; leave any IMPLIES in the hypotheses. These IMPLIES are thought to
; have been introduced by :USE hints.
(let ((term (disjoin (expand-any-final-implies cl wrld))))
(mv-let (term ttree)
(expand-abbreviations term nil
*geneqv-iff*
(access rewrite-constant
rcnst
:fns-to-be-ignored-by-rewrite)
(rewrite-stack-limit wrld)
(access rewrite-constant
rcnst
:current-enabled-structure)
wrld state nil)
(mv-let (clauses ttree)
(clausify-input term
(access rewrite-constant
(access prove-spec-var
pspv
:rewrite-constant)
:fns-to-be-ignored-by-rewrite)
(access rewrite-constant
rcnst
:current-enabled-structure)
wrld
state
ttree)
;;; (let ((clauses
;;; (expand-some-non-rec-fns-in-clauses
;;; '(iff implies)
;;; clauses
;;; wrld)))
#| Previous to Version_2.6 we had written:
; Note: Once upon a time (in Version 1.5) we called "clausify-clause-set" here.
; That function called clausify on each element of clauses and unioned the
; results together, in the process naturally deleting tautologies as does
; expand-some-non-rec-fns-in-clauses above. But Version 1.5 caused Bishop a
; lot of pain because many theorems would explode into case analyses, each of
; which was then dispatched by simplification. The reason we used a full-blown
; clausify in Version 1.5 was that in was also into that version that we
; introduced forcing rounds and the liberal use of force-flg = t. But if we
; are to force that way, we must really get all of our hypotheses out into the
; open so that they can contribute to the type-alist stored in each assumption.
; For example, in Version 1.4 the concl of (IMPLIES hyps concl) was rewritten
; first without the hyps being manifest in the type-alist since IMPLIES is a
; function. Not until the IMPLIES was opened did the hyps become "governers"
; in this sense. In Version 1.5 we decided to throw caution to the wind and
; just clausify the clausified input. Well, it bit us as mentioned above and
; we are now backing off to simply expanding the non-rec fns that might
; contribute hyps. But we leave the expansions in place rather than normalize
; them out so that simplification has one shot on a small set (usually
; singleton set) of clauses.
|#
; But the comment above is now irrelevant to the current situation.
; Before commenting on the current situation, however, we point out that
; in (admittedly light) testing the original call to
; expand-some-non-rec-fns-in-clauses in its original context acted as
; the identity. This seems reasonable because 'iff and 'implies were
; expanded in expand-abbreviations.
; We now expand the 'implies from the original theorem (but not the
; implies from a :use hint) in the call to expand-any-final-implies.
; This performs the expansion whose motivations are mentioned in the
; old comments above, but does not interfere with the conclusions
; of a :use hint. See the mini-essay
; Mini-Essay on Assume-true-false-if and Implies
; or
; How Strengthening One Part of a Theorem Prover Can Weaken the Whole.
; in type-set-b for more details on this latter criterion.
(cond
((equal clauses (list cl))
; In this case, preprocess-clause has made no changes to the clause.
(mv 'miss nil nil nil))
((and (consp clauses)
(null (cdr clauses))
(no-op-histp hist)
(equal (prettyify-clause
(car clauses)
(let*-abstractionp state)
wrld)
(access prove-spec-var pspv
:displayed-goal)))
; In this case preprocess-clause has produced a singleton set of
; clauses whose only element will be displayed exactly like what the
; user thinks is the input to prove. For example, the user might have
; invoked defthm on (implies p q) and preprocess has managed to to
; produce the singleton set of clauses containing {(not p) q}. This
; is a valuable step in the proof of course. However, users complain
; when we report that (IMPLIES P Q) -- the displayed goal -- is
; reduced to (IMPLIES P Q) -- the prettyification of the output.
; We therefore take special steps to hide this transformation from the
; user without changing the flow of control through the waterfall. In
; particular, we will insert into the ttree the tag
; 'hidden-clause with (irrelevant) value t. In subsequent places
; where we print explanations and clauses to the user we will look for
; this tag.
(mv 'hit
clauses
(add-to-tag-tree
'hidden-clause t ttree)
pspv))
(t (mv 'hit
clauses
ttree
pspv)))))))))))
(defun preprocess-clause-msg1 (signal clauses ttree pspv state)
; This function is one of the waterfall-msg subroutines. It has the
; standard arguments of all such functions: the signal, clauses, ttree
; and pspv produced by the given processor, in this case
; preprocess-clause. It produces the report for this step.
(declare (ignore signal pspv))
(cond ((tag-tree-occur 'hidden-clause t ttree)
; If this preprocess clause is to be hidden, e.g., because it transforms
; (IMPLIES P Q) to {(NOT P) Q}, we print no message. Note that this is
; just part of the hiding. Later in the waterfall, when some other processor
; has successfully hit our output, that output will be printed and we
; need to stop that printing too.
state)
((null clauses)
(fms "But we reduce the conjecture to T, by ~*0.~|"
(list (cons #\0 (tilde-*-preprocess-phrase ttree)))
(proofs-co state)
state
(term-evisc-tuple nil state)))
(t
(fms "By ~*0 we reduce the conjecture to~#1~[~x2.~/~/ the following ~
~n3 conjectures.~]~|"
(list (cons #\0 (tilde-*-preprocess-phrase ttree))
(cons #\1 (zero-one-or-more clauses))
(cons #\2 t)
(cons #\3 (length clauses)))
(proofs-co state)
state
(term-evisc-tuple nil state)))))
(defun apply-use-hint-clauses (temp clauses pspv wrld state)
; Note: There is no apply-use-hint-clause. We just call this function
; on a singleton list of clauses.
; Temp is the result of assoc-eq :use in a pspv :hint-settings and is
; non-nil. We discuss its shape below. But this function applies the
; given :use hint to each clause in clauses and returns (mv 'hit
; new-clauses ttree new-pspv).
; Temp is of the form (:USE lmi-lst (hyp1 ... hypn) constraint-cl k
; event-names new-entries) where each hypi is a theorem and
; constraint-cl is a clause that expresses the conjunction of all k
; constraints. Lmi-lst is the list of lmis that generated these hyps.
; Constraint-cl is (probably) of the form {(if constr1 (if constr2 ...
; (if constrk t nil)... nil) nil)}. We add each hypi as a hypothesis
; to each goal clause, cl, and in addition, create one new goal for
; each constraint. Note that we discard the extended goal clause if
; it is a tautology. Note too that the constraints generated by the
; production of the hyps are conjoined into a single clause in temp.
; But we hit that constraint-cl with preprocess-clause to pick out its
; (non-tautologial) cases and that code will readily unpack the if
; structure of a typical conjunct. We remove the :use hint from the
; hint-settings so we don't fire the same :use again on the subgoals.
; We return (mv 'hit new-clauses ttree new-pspv).
; The ttree returned has at most two tags. The first is :use and has
; ((lmi-lst hyps constraint-cl k event-names new-entries)
; . non-tautp-applications) as its value, where non-tautp-applications
; is the number of non-tautologous clauses we got by adding the hypi
; to each clause. However, it is possible the :use tag is not
; present: if clauses is nil, we don't report a :use. The optional
; second tag is the ttree produced by preprocess-clause on the
; constraint-cl. If the preprocess-clause is to be hidden anyway, we
; ignore its tree (but use its clauses).
(let* ((hyps (caddr temp))
(constraint-cl (cadddr temp))
(new-pspv (change prove-spec-var pspv
:hint-settings
(remove1-equal temp
(access prove-spec-var
pspv
:hint-settings))))
(A (disjoin-clause-segment-to-clause-set (dumb-negate-lit-lst hyps)
clauses))
(non-tautp-applications (length A)))
; In this treatment, the final set of goal clauses will the union of
; sets A and C. A stands for the "application clauses" (obtained by
; adding the use hyps to each clause) and C stands for the "constraint
; clauses." Non-tautp-applications is |A|.
(cond
((null clauses)
; In this case, there is no point in generating the constraints! We
; anticipate this happening if the user provides both a :use and a
; :cases hint and the :cases hint (which is applied first) proves the
; goal completely. If that were to happen, clauses would be output of
; the :cases hint and pspv would be its output pspv, from which the
; :cases had been deleted. So we just delete the :use hint from that
; pspv and call it quits, without reporting a :use hint at all.
(mv 'hit nil nil new-pspv))
(t
(mv-let
(signal C ttree irrel-pspv)
(preprocess-clause constraint-cl nil pspv wrld state)
(declare (ignore irrel-pspv))
(cond
((eq signal 'miss)
(mv 'hit
(conjoin-clause-sets
A
(conjoin-clause-to-clause-set constraint-cl
nil))
(add-to-tag-tree :use
(cons (cdr temp)
non-tautp-applications)
nil)
new-pspv))
((or (tag-tree-occur 'hidden-clause
t
ttree)
(and C
(null (cdr C))
(equal (list (prettyify-clause
(car C)
(let*-abstractionp state)
wrld))
constraint-cl)))
(mv 'hit
(conjoin-clause-sets A C)
(add-to-tag-tree :use
(cons (cdr temp)
non-tautp-applications)
nil)
new-pspv))
(t (mv 'hit
(conjoin-clause-sets A C)
(add-to-tag-tree :use
(cons (cdr temp)
non-tautp-applications)
(add-to-tag-tree 'preprocess-ttree
ttree
nil))
new-pspv))))))))
(defun apply-top-hints-clause1 (temp cl-id cl pspv wrld state)
; See apply-top-hints-clause. This handles the case that we found a
; hint-setting, temp, for a top hint other than :clause-processor.
(case (car temp)
(:use ; temp is a non-nil :use hint.
(let ((cases-temp
(assoc-eq :cases
(access prove-spec-var pspv :hint-settings))))
(cond
((null cases-temp)
(apply-use-hint-clauses temp (list cl) pspv wrld state))
(t
; In this case, we have both :use and :cases hints. Our
; interpretation of this is that we split clause cl according to the
; :cases and then apply the :use hint to each case. By the way, we
; don't have to consider the possibility of our having a :use and :by
; or :bdd. That is ruled out by translate-hints.
(mv-let
(signal cases-clauses cases-ttree cases-pspv)
(apply-cases-hint-clause cases-temp cl pspv wrld)
(declare (ignore signal))
; We know the signal is 'HIT.
(mv-let
(signal use-clauses use-ttree use-pspv)
(apply-use-hint-clauses temp
cases-clauses
cases-pspv
wrld state)
(declare (ignore signal))
; Despite the names, use-clauses and use-pspv both reflect the work we
; did for cases. However, use-ttree was built from scratch as was
; cases-ttree and we must combine them.
(mv 'HIT
use-clauses
(cons-tag-trees use-ttree cases-ttree)
use-pspv)))))))
(:by
; If there is a :by hint then it is of one of the two forms (:by . name) or
; (:by lmi-lst thm constraint-cl k event-names new-entries). The first form
; indicates that we are to give this clause a bye and let the proof fail late.
; The second form indicates that the clause is supposed to be subsumed by thm,
; viewed as a set of clauses, but that we have to prove constraint-cl to obtain
; thm and that constraint-cl is really a conjunction of k constraints. Lmi-lst
; is a singleton list containing the lmi that generated this thm-cl.
(cond
((symbolp (cdr temp))
; So this is of the first form, (:by . name). We want the proof to fail, but
; not now. So we act as though we proved cl (we hit, produce no new clauses
; and don't change the pspv) but we return a tag tree containing the tag
; :bye with the value (name . cl). At the end of the proof we must search
; the tag tree and see if there are any :byes in it. If so, the proof failed
; and we should display the named clauses.
(mv 'hit
nil
(add-to-tag-tree :bye (cons (cdr temp) cl) nil)
pspv))
(t
(let ((lmi-lst (cadr temp)) ; a singleton list
(thm (caddr temp))
(constraint-cl (cadddr temp))
(new-pspv
(change prove-spec-var pspv
:hint-settings
(remove1-equal temp
(access prove-spec-var
pspv
:hint-settings)))))
; We remove the :by from the hint-settings. Why do we remove the :by?
; If we don't the subgoals we create from constraint-cl will also see
; the :by!
; We insist that thm-cl-set subsume cl -- more precisely, that cl be
; subsumed by some member of thm-cl-set.
; WARNING: See the warning about the processing in translate-by-hint.
(let* ((easy-winp
(if (and cl (null (cdr cl)))
(equal (car cl) thm)
(equal thm
(implicate
(conjoin (dumb-negate-lit-lst (butlast cl 1)))
(car (last cl))))))
(cl1 (if (and (not easy-winp)
(ffnnamep-lst 'implies cl))
(expand-some-non-rec-fns-lst '(implies) cl wrld)
cl))
(cl-set (if (not easy-winp)
; Before Version_2.7 we only called clausify here when (and (null hist) cl1
; (null (cdr cl1))). But Robert Krug sent an example in which a :by hint was
; given on a subgoal that had been produced from "Goal" by destructor
; elimination. That subgoal was identical to the theorem given in the :by
; hint, and hence easy-winp is true; but before Version_2.7 we did not look for
; the easy win. So, what happened was that thm-cl-set was the result of
; clausifying the theorem given in the :by hint, but cl-set was a singleton
; containing cl1, which still has IF terms.
(clausify (disjoin cl1) nil t wrld)
(list cl1)))
(thm-cl-set (if easy-winp
(list (list thm))
; WARNING: Below we process the thm obtained from the lmi. In particular, we
; expand certain non-rec fns and we clausify it. For heuristic sanity, the
; processing done here should exactly duplicate that done above for cl-set.
; The reason is that we want it to be the case that if the user gives a :by
; hint that is identical to the goal theorem, the subsumption is guaranteed to
; succeed. If the processing of the goal theorem is slightly different than
; the processing of the hint, that guarantee is invalid.
(clausify (expand-some-non-rec-fns
'(implies) thm wrld)
nil
t
wrld)))
(val (list* (cadr temp) thm-cl-set (cdddr temp)))
(subsumes (and (not easy-winp) ; otherwise we don't care
(clause-set-subsumes nil
; We supply nil just above, rather than (say) *init-subsumes-count*, because
; the user will be able to see that if the subsumption check goes out to lunch
; then it must be because of the :by hint. For example, it takes 167,997,825
; calls of one-way-unify1 (more than 2^27, not far from the fixnum limit in
; many Lisps) to do the subsumption check for the following, yet in a feasible
; time (26 seconds on Allegro CL 7.0, on a 2.6GH Pentium 4). So we prefer not
; to set a limit.
; (defstub p (x) t)
; (defstub s (x1 x2 x3 x4 x5 x6 x7 x8) t)
; (defaxiom ax
; (implies (and (p x1) (p x2) (p x3) (p x4)
; (p x5) (p x6) (p x7) (p x8))
; (s x1 x2 x3 x4 x5 x6 x7 x8))
; :rule-classes nil)
; (defthm prop
; (implies (and (p x1) (p x2) (p x3) (p x4)
; (p x5) (p x6) (p x7) (p x8))
; (s x8 x7 x3 x4 x5 x6 x1 x2))
; :hints (("Goal" :by ax)))
thm-cl-set cl-set)))
(success (or easy-winp subsumes)))
; Before the full-blown subsumption check we ask if the two sets are identical
; and also if they are each singleton sets and the thm-cl-set's clause is a
; subset of the other clause. These are fast and commonly successful checks.
(cond
(success
; Ok! We won! To produce constraint-cl as our goal we first
; preprocess it as though it had come down from the top. See the
; handling of :use hints below for some comments on this. This code
; was copied from that historically older code.
(mv-let (signal clauses ttree irrel-pspv)
(preprocess-clause constraint-cl nil pspv wrld
state)
(declare (ignore irrel-pspv))
(cond ((eq signal 'miss)
(mv 'hit
(conjoin-clause-to-clause-set
constraint-cl nil)
(add-to-tag-tree :by val nil)
new-pspv))
((or (tag-tree-occur 'hidden-clause
t
ttree)
(and clauses
(null (cdr clauses))
(equal (list
(prettyify-clause
(car clauses)
(let*-abstractionp state)
wrld))
constraint-cl)))
; If preprocessing produced a single clause that prettyifies to the
; clause we had, then act as though it didn't do anything (but use its
; output clause set). This is akin to the 'hidden-clause
; hack of preprocess-clause, which, however, is intimately tied to the
; displayed-goal input to prove and not to the input to prettyify-
; clause. We look for the 'hidden-clause tag just in case.
(mv 'hit
clauses
(add-to-tag-tree :by val nil)
new-pspv))
(t
(mv 'hit
clauses
(add-to-tag-tree
:by val
(add-to-tag-tree 'preprocess-ttree
ttree
nil))
new-pspv)))))
(t (mv 'error
(msg "When a :by hint is used to supply a ~
lemma-instance for a given goal-spec, the ~
formula denoted by the lemma-instance must ~
subsume the goal. This did not happen~@1! ~
The lemma-instance provided was ~x0, which ~
denotes the formula ~P24 (when converted to a ~
set of clauses and then printed as a formula). ~
This formula was not found to subsume the ~
goal clause, ~P34.~|~%Consider a :use hint ~
instead ; see :DOC hints."
(car lmi-lst)
; The following is not possible, because we are not putting a limit on the
; number of one-way-unify1 calls in our subsumption check (see above). But we
; leave this code here in case we change our minds on that.
(if (eq subsumes '?)
" because our subsumption heuristics were ~
unable to decide the question"
"")
(untranslate thm t wrld)
(prettyify-clause-set cl-set
(let*-abstractionp state)
wrld)
nil)
nil
nil))))))))
(:cases
; Then there is no :use hint present. See the comment in *top-hint-keywords*.
(apply-cases-hint-clause temp cl pspv wrld))
(:bdd
(bdd-clause (cdr temp) cl-id cl
(change prove-spec-var pspv
:hint-settings
(remove1-equal temp
(access prove-spec-var
pspv
:hint-settings)))
wrld state))
(t (mv (er hard 'apply-top-hints-clause.
"Implementation error: Missing case in apply-top-hints-clause.")
nil nil nil))))
(defun apply-top-hints-clause (cl-id cl hist pspv wrld ctx state)
; This is a standard clause processor of the waterfall. It is odd in that it
; is a no-op unless there is a :use, :by, :cases, :bdd, or :clause-processor
; hint in the :hint-settings of pspv. If there is, we remove it and apply it.
; By implementing these hints via this special-purpose processor we can take
; advantage of the waterfall's already-provided mechanisms for handling
; multiple clauses and output.
; We return 4 values. The first is a signal that is either 'hit, 'miss, or
; 'error. When the signal is 'miss, the other 3 values are irrelevant. When
; the signal is 'error, the second result is a pair of the form (str . alist)
; which allows us to give our caller an error message to print. In this case,
; the other two values are irrelevant. When the signal is 'hit, the second
; result is the list of new clauses, the third is a ttree that will become that
; component of the history-entry for this process, and the fourth is the
; modified pspv.
; We need cl-id passed in so that we can store it in the bddnote, in the case
; of a :bdd hint.
(declare (ignore hist))
(let ((temp (first-assoc-eq *top-hint-keywords*
(access prove-spec-var pspv
:hint-settings))))
(cond
((null temp) (mv 'miss nil nil nil state))
((eq (car temp) :clause-processor) ; special case since state is returned
; Temp is of the form (:clause-processor term . stobjs-out), as returned by
; translate-clause-processor-hint.
(mv-let
(erp new-clauses state)
(eval-clause-processor cl
(access clause-processor-hint (cdr temp) :term)
(access clause-processor-hint (cdr temp) :stobjs-out)
ctx state)
(cond (erp (mv 'error erp nil nil state))
(t (mv 'hit
new-clauses
(cond ((and new-clauses
(null (cdr new-clauses))
(equal (car new-clauses) cl))
(add-to-tag-tree 'hidden-clause t nil))
(t (add-to-tag-tree
:clause-processor
(cons (cdr temp) new-clauses)
nil)))
(change prove-spec-var pspv
:hint-settings
(remove1-equal temp
(access prove-spec-var
pspv
:hint-settings)))
state)))))
(t (mv-let
(signal clauses ttree new-pspv)
(apply-top-hints-clause1 temp cl-id cl pspv wrld state)
(mv signal clauses ttree new-pspv state))))))
(defun apply-top-hints-clause-msg1
(signal cl-id clauses speciousp ttree pspv state)
; This function is one of the waterfall-msg subroutines. It has the standard
; arguments of all such functions: the signal, clauses, ttree and pspv produced
; by the given processor, in this case preprocess-clause (except that for bdd
; processing, the ttree comes from bdd-clause, which is similar to
; simplify-clause, which explains why we also pass in the argument speciousp).
; It produces the report for this step.
; Note: signal and pspv are really ignored, but they don't appear to be when
; they are passed to simplify-clause-msg1 below, so we cannot declare them
; ignored here.
(cond ((tagged-object :bye ttree)
; The object associated with the :bye tag is (name . cl). We are interested
; only in name here.
(fms "But we have been asked to pretend that this goal is ~
subsumed by the as-yet-to-be-proved ~x0.~|"
(list (cons #\0 (car (cdr (tagged-object :bye ttree)))))
(proofs-co state)
state
nil))
((tagged-object :by ttree)
(let* ((obj (cdr (tagged-object :by ttree)))
; Obj is of the form (lmi-lst thm-cl-set constraint-cl k event-names
; new-entries).
(lmi-lst (car obj))
(thm-cl-set (cadr obj))
(k (car (cdddr obj)))
(event-names (cadr (cdddr obj)))
(ttree (cdr (tagged-object 'preprocess-ttree ttree))))
(fms "~#0~[But, as~/As~/As~] indicated by the hint, this goal is ~
subsumed by ~P18, which ~@2.~#3~[~/ By ~*4 we reduce the ~
~#5~[constraint~/~n6 constraints~] to ~#0~[T~/the following ~
conjecture~/the following ~n7 conjectures~].~]~|"
(list (cons #\0 (zero-one-or-more clauses))
(cons #\1 (prettyify-clause-set
thm-cl-set
(let*-abstractionp state)
(w state)))
(cons #\2 (tilde-@-lmi-phrase lmi-lst k event-names))
(cons #\3 (if (int= k 0) 0 1))
(cons #\4 (tilde-*-preprocess-phrase ttree))
(cons #\5 (if (int= k 1) 0 1))
(cons #\6 k)
(cons #\7 (length clauses))
(cons #\8 nil))
(proofs-co state)
state
(term-evisc-tuple nil state))))
((tagged-object :use ttree)
(let* ((use-obj (cdr (tagged-object :use ttree)))
; The presence of :use indicates that a :use hint was applied to one
; or more clauses to give the output clauses. If there is also a
; :cases tag in the ttree, then the input clause was split into to 2
; or more cases first and then the :use hint was applied to each. If
; there is no :cases tag, the :use hint was applied to the input
; clause alone. Each application of the :use hint adds literals to
; the target clause(s). This generates a set, A, of ``applications''
; but A need not be the same length as the set of clauses to which we
; applied the :use hint since some of those applications might be
; tautologies. In addition, the :use hint generated some constraints,
; C. The set of output clauses, say G, is (C U A). But C and A are
; not necessarily disjoint, e.g., some constraints might happen to be
; in A. Once upon a time, we reported on the number of non-A
; constraints, i.e., |C'|, where C' = C\A. Because of the complexity
; of the grammar, we do not reveal to the user all the numbers: how
; many non-tautological cases, how many hypotheses, how many
; non-tautological applications, how many constraints generated, how
; many after preprocessing the constraints, how many overlaps between
; C and A, etc. Instead, we give a fairly generic message. But we
; have left (as comments) the calculation of the key numbers in case
; someday we revisit this.
; The shape of the use-obj, which is the value of the :use tag, is
; ((lmi-lst (hyp1 ...) cl k event-names new-entries)
; . non-tautp-applications) where non-tautp-applications is the number
; of non-tautologies created by the one or more applications of the
; :use hint, i.e., |A|. (But we do not report this.)
(lmi-lst (car (car use-obj)))
(hyps (cadr (car use-obj)))
(k (car (cdddr (car use-obj)))) ;;; |C|
(event-names (cadr (cdddr (car use-obj))))
; (non-tautp-applications (cdr use-obj)) ;;; |A|
(preprocess-ttree
(cdr (tagged-object 'preprocess-ttree ttree)))
; (len-A non-tautp-applications) ;;; |A|
(len-G (len clauses)) ;;; |G|
(len-C k) ;;; |C|
; (len-C-prime (- len-G len-A)) ;;; |C'|
(cases-obj (cdr (tagged-object :cases ttree)))
; If there is a cases-obj it means we had a :cases and a :use; the
; form of cases-obj is (splitting-terms . case-clauses), where
; case-clauses is the result of splitting on the literals in
; splitting-terms. We know that case-clauses is non-nil. (Had it
; been nil, no :use would have been reported.) Note that if cases-obj
; is nil, i.e., there was no :cases hint applied, then these next two
; are just nil. But we'll want to ignore them if cases-obj is nil.
; (splitting-terms (car cases-obj))
; (case-clauses (cdr cases-obj))
)
(fms
"~#0~[But we~/We~] ~
~#x~[split the goal into the cases specified by ~
the :CASES hint and augment each case~
~/~
augment the goal~] ~
with the ~#1~[hypothesis~/hypotheses~] provided by ~
the :USE hint. ~#1~[The hypothesis~/These hypotheses~] ~
~@2~
~#3~[~/; the constraint~#4~[~/s~] can be ~
simplified using ~*5~]. ~
~#6~[This reduces the goal to T.~/~
We are left with the following subgoal.~/~
We are left with the following ~n7 subgoals.~]~%"
(list
(cons #\x (if cases-obj 0 1))
(cons #\0 (if (> len-G 0) 1 0)) ;;; |G|>0
(cons #\1 hyps)
(cons #\2 (tilde-@-lmi-phrase lmi-lst k event-names))
(cons #\3 (if (> len-C 0) 1 0)) ;;; |C|>0
(cons #\4 (if (> len-C 1) 1 0)) ;;; |C|>1
(cons #\5 (tilde-*-preprocess-phrase preprocess-ttree))
(cons #\6 (if (equal len-G 0) 0 (if (equal len-G 1) 1 2)))
(cons #\7 len-G))
(proofs-co state)
state
(term-evisc-tuple nil state))))
((tagged-object :cases ttree)
(let* ((cases-obj (cdr (tagged-object :cases ttree)))
; The cases-obj here is of the form (term-list . new-clauses), where
; new-clauses is the result of splitting on the literals in term-list.
; (splitting-terms (car cases-obj))
(new-clauses (cdr cases-obj)))
(cond
(new-clauses
(fms "We now split the goal into the cases specified by ~
the :CASES hint to produce ~n0 new non-trivial ~
subgoal~#1~[~/s~].~|"
(list (cons #\0 (length new-clauses))
(cons #\1 (if (cdr new-clauses) 1 0)))
(proofs-co state)
state
(term-evisc-tuple nil state)))
(t
(fms "But the resulting goals are all true by case reasoning."
nil
(proofs-co state)
state
nil)))))
((tagged-object 'hidden-clause ttree)
state)
((tagged-object :clause-processor ttree)
(let* ((clause-processor-obj (cdr (tagged-object :clause-processor ttree)))
; The clause-processor-obj here is produced by apply-top-hints-clause, and is
; of the form (clause-processor-hint . new-clauses), where new-clauses is the
; result of splitting on the literals in term-list and hint is the translated
; form of a :clause-processor hint.
(verified-p (access clause-processor-hint
(car clause-processor-obj)
:verified-p))
(new-clauses (cdr clause-processor-obj)))
(cond
(new-clauses
(fms "We now apply the ~@0 :CLAUSE-PROCESSOR function ~x1 to produce ~
~n2 new subgoal~#3~[~/s~].~|"
(list (cons #\0 (cond (verified-p "verified")
(t "trusted")))
(cons #\1 (ffn-symb (access clause-processor-hint
(car clause-processor-obj)
:term)))
(cons #\2 (length new-clauses))
(cons #\3 (if (cdr new-clauses) 1 0)))
(proofs-co state)
state
(term-evisc-tuple nil state)))
(t
(fms "But the supplied :CLAUSE-PROCESSOR hint replaces this goal ~
by T.~|"
nil
(proofs-co state)
state
nil)))))
(t
; Normally we expect (tagged-object 'bddnote ttree) in this case, but it is
; possible that forward-chaining after trivial equivalence removal proved
; the clause, without actually resorting to bdd processing.
(simplify-clause-msg1 signal cl-id clauses speciousp ttree pspv
state))))
(defun more-than-simplifiedp (hist)
; Return t if hist contains a process besides simplify-clause (and its
; mates settled-down-clause and preprocess-clause).
(cond ((null hist) nil)
((member-eq (caar hist) '(settled-down-clause
simplify-clause
preprocess-clause))
(more-than-simplifiedp (cdr hist)))
((eq (caar hist) 'apply-top-hints-clause)
(if (tagged-object 'hidden-clause
(access history-entry (car hist) :ttree))
(more-than-simplifiedp (cdr hist))
t))
(t t)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Fix for :PL bugs
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defun pc-relieve-hyp (rune hyp unify-subst type-alist wrld state ens ttree)
; This function is adapted from ACL2 function relieve-hyp, but it prevents
; backchaining, instead returning the new hypotheses. Notice that there are no
; arguments for obj, equiv, fnstack, ancestors, or simplify-clause-pot-lst.
; Also notice that rcnst has been replaced by ens (an enable structure).
; We return t or nil indicating whether we won, an extended unify-subst
; and a new ttree. This function is a No-Change Loser.
(cond ((f-big-clock-negative-p state)
(mv nil unify-subst ttree))
((and (nvariablep hyp)
(not (fquotep hyp))
(eq (ffn-symb hyp) 'synp))
(mv-let
(wonp failure-reason unify-subst ttree)
(relieve-hyp-synp rune hyp unify-subst
(rewrite-stack-limit wrld)
type-alist
wrld
state
nil ; fnstack
nil ; ancestors
nil ; backchain-limit
nil ; simplify-clause-pot-lst
(make-rcnst ens
wrld
:force-info 'weak) ; conservative
nil ; gstack
ttree)
(declare (ignore failure-reason))
(mv wonp unify-subst ttree)))
(t (mv-let
(forcep bind-flg)
(binding-hyp-p hyp unify-subst wrld)
(let ((hyp (if forcep (fargn hyp 1) hyp)))
(cond
(bind-flg
(mv t
(cons (cons (fargn hyp 1) (fargn hyp 2))
unify-subst)
ttree))
(t
(mv-let
(lookup-hyp-ans unify-subst ttree)
(lookup-hyp hyp type-alist wrld unify-subst ttree)
(cond
(lookup-hyp-ans
(mv t unify-subst ttree))
((free-varsp hyp unify-subst)
(search-ground-units` hyp unify-subst type-alist ens
(ok-to-force-ens ens) wrld ttree))
(t
(let ((inst-hyp (sublis-var unify-subst hyp)))
(mv-let
(knownp nilp nilp-ttree)
(known-whether-nil inst-hyp type-alist ens
(ok-to-force-ens ens) wrld ttree)
(cond
(knownp
(mv (not nilp) unify-subst nilp-ttree))
(t
(mv-let
(not-flg atm)
(strip-not hyp)
; Again, we avoid rewriting in this proof-checker code.
(cond
(not-flg
(if (equal atm *nil*)
(mv t unify-subst ttree)
(mv nil unify-subst ttree)))
(t
(if (if-tautologyp atm)
(mv t unify-subst ttree)
(mv nil unify-subst ttree)))))))))))))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Improvements to :accumulated-persistence
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defrec accp-entry
; The "s" and "f" suffices below suggest "success" and "failure", though a
; better distinction is between "useful work" and "useless work". Our
; user-level reports say "useful" and "useless".
(rune . ((n-s . ap-s)
.
(n-f . ap-f)))
t)
(defrec accp-info
; The "s" and "f" suffices below suggest "success" and "failure", though a
; better distinction is between "useful work" and "useless work". Our
; user-level reports say "useful" and "useless".
(((cnt-s . cnt-f) . (stack-s . stack-f))
.
totals)
t)
(defabbrev rune= (rune1 rune2)
(and (eq (car rune1) (car rune2))
(equal (cdr rune1) (cdr rune2))))
(defun merge-accumulated-persistence-aux (rune entry alist)
(cond ((endp alist)
; See the comment below merge-accumulated-persistence for an attempt we made to
; avoid this unfortunate case (unfortunate because we consed up a new alist
; rather than just pushing the entry on the front).
(list entry))
((rune= rune (access accp-entry (car alist) :rune))
(cons (make accp-entry
:rune rune
:n-s (+ (access accp-entry entry :n-s)
(access accp-entry (car alist) :n-s))
:ap-s (+ (access accp-entry entry :ap-s)
(access accp-entry (car alist) :ap-s))
:n-f (+ (access accp-entry entry :n-f)
(access accp-entry (car alist) :n-f))
:ap-f (+ (access accp-entry entry :ap-f)
(access accp-entry (car alist) :ap-f)))
(cdr alist)))
(t (cons (car alist)
(merge-accumulated-persistence-aux rune entry (cdr alist))))))
(defun merge-accumulated-persistence-rec (new-alist old-alist)
(cond ((endp new-alist) old-alist)
(t (merge-accumulated-persistence-rec
(cdr new-alist)
(merge-accumulated-persistence-aux
(access accp-entry (car new-alist) :rune)
(car new-alist)
old-alist)))))
(defun merge-accumulated-persistence (new-alist old-alist)
; We tried an approach using sorting with rune-<, but it was much more
; expensive. We used as an example:
; cd books/workshops/2004/legato/support/
; acl2::(set-inhibit-output-lst '(prove proof-tree))
; (accumulated-persistence t)
; (time$ (ld "proof-by-generalization-mult.lisp"))
; All timings below are in GCL 2.6.7.
; Using rune-<:
; real time : 198.170 secs
; run-gbc time : 186.320 secs
; child run time : 0.000 secs
; gbc time : 7.720 secs
; Using the present approach, without sorting:
; real time : 141.170 secs
; run-gbc time : 129.070 secs
; child run time : 0.000 secs
; gbc time : 7.900 secs
; Approach through Version_3.2, without accounting for successes/failures:
; real time : 137.140 secs
; run-gbc time : 127.410 secs
; child run time : 0.000 secs
; gbc time : 5.930 secs
; See also below for alternate approach that didn't do as well.
(cond ((null old-alist) ; optimization
new-alist)
(t (merge-accumulated-persistence-rec new-alist old-alist))))
#||
The following alternate code doesn't do as well, even though it uses nconc.
The nconc version doesn't even seem much better on space (in fact worse in an
Allegro CL test as reported by "space allocation": 669,110,675 cons cells in
the nconc version vs. 593,299,188). Compare the times below with those
reported in merge-accumulated-persistence.
Our basic idea was to avoid walking consing up a new alist in
merge-accumulated-persistence-aux when the given rune wasn't already a key in
the given alist.
real time : 157.780 secs
run-gbc time : 146.960 secs
child run time : 0.000 secs
gbc time : 8.990 secs
Replacing nconc with revappend:
real time : 168.870 secs
run-gbc time : 149.930 secs
child run time : 0.000 secs
gbc time : 8.930 secs
(defun merge-accumulated-persistence-1 (rune entry alist)
(cond ((endp alist)
(er hard 'merge-accumulated-persistence-1
"Implementation error: Unexpected end of list! Please contacct ~
the ACL2 implementors."))
((rune= rune (access accp-entry (car alist) :rune))
(cons (make accp-entry
:rune rune
:n-s (+ (access accp-entry entry :n-s)
(access accp-entry (car alist) :n-s))
:ap-s (+ (access accp-entry entry :ap-s)
(access accp-entry (car alist) :ap-s))
:n-f (+ (access accp-entry entry :n-f)
(access accp-entry (car alist) :n-f))
:ap-f (+ (access accp-entry entry :ap-f)
(access accp-entry (car alist) :ap-f)))
(cdr alist)))
(t (cons (car alist)
(merge-accumulated-persistence-1 rune entry (cdr alist))))))
(defun assoc-rune= (rune alist)
(cond ((endp alist) nil)
((rune= rune (access accp-entry (car alist) :rune))
(car alist))
(t (assoc-rune= rune (cdr alist)))))
(defun merge-accumulated-persistence-rec (new-alist old-alist new-alist-new)
; We merge into old-alist as we go along, except that entries in new-alist that
; are not in old-alist are put into new-alist-new.
(cond ((endp new-alist) (nconc new-alist-new old-alist))
(t (let* ((rune (access accp-entry (car new-alist) :rune))
(pair (assoc-rune= rune old-alist)))
(merge-accumulated-persistence-rec
(cdr new-alist)
(cond (pair (merge-accumulated-persistence-1
rune
(car new-alist)
old-alist))
(t old-alist))
(cond (pair new-alist-new)
(t (cons (car new-alist) new-alist-new))))))))
; Also would need to add final argument of nil to call of
; merge-accumulated-persistence-rec in merge-accumulated-persistence.
||#
(defun add-accumulated-persistence-s (rune delta-s delta-f alist original-alist
acc)
; Warning: Keep this in sync with add-accumulated-persistence-f.
(cond ((null alist)
(cons (make accp-entry
:rune rune
:n-s 1
:ap-s delta-s
:n-f 0
:ap-f delta-f)
original-alist))
((rune= rune (access accp-entry (car alist) :rune))
(cons (change accp-entry (car alist)
:n-s (1+ (access accp-entry (car alist) :n-s))
:ap-s (+ delta-s (access accp-entry (car alist)
:ap-s))
:ap-f (+ delta-f (access accp-entry (car alist)
:ap-f)))
(revappend acc (cdr alist))))
(t (add-accumulated-persistence-s
rune delta-s delta-f (cdr alist) original-alist
(cons (car alist) acc)))))
(defun add-accumulated-persistence-f (rune delta-s delta-f alist original-alist
acc)
; Warning: Keep this in sync with add-accumulated-persistence-s.
(cond ((null alist)
(cons (make accp-entry
:rune rune
:n-s 0
:ap-s 0
:n-f 1
:ap-f (+ delta-f delta-s))
original-alist))
((rune= rune (access accp-entry (car alist) :rune))
(cons (change accp-entry (car alist)
:n-f (1+ (access accp-entry (car alist) :n-f))
:ap-f (+ delta-s delta-f
(access accp-entry (car alist)
:ap-s)
(access accp-entry (car alist)
:ap-f)))
(revappend acc (cdr alist))))
(t (add-accumulated-persistence-f
rune delta-s delta-f (cdr alist) original-alist
(cons (car alist) acc)))))
(defun accumulated-persistence-make-failures (alist)
(cond ((null alist) nil)
(t
(cons (change accp-entry (car alist)
:n-f (+ (access accp-entry (car alist) :n-f)
(access accp-entry (car alist) :n-s))
:n-s 0
:ap-f (+ (access accp-entry (car alist) :ap-f)
(access accp-entry (car alist) :ap-s))
:ap-s 0)
(accumulated-persistence-make-failures (cdr alist))))))
(defun add-accumulated-persistence (rune success-p delta-s delta-f alist-stack)
; Alist-stack is a list of lists of accp-entry records. First, we modify the
; top of alist-stack to record everything as useless (failure) if success-p is
; nil. Then, we merge that modification into the second element of
; alist-stack, after incrementing by 1 for the given rune's :n-s or :n-f and by
; delta for its :ap-s or :ap-f, according to success-p.
(assert$
(cdr alist-stack)
(let* ((alist (if success-p
(car alist-stack)
(accumulated-persistence-make-failures (car alist-stack))))
(new-alist (cond
(success-p
(add-accumulated-persistence-s
rune delta-s delta-f alist alist nil))
(t
(add-accumulated-persistence-f
rune delta-s delta-f alist alist nil)))))
(cons (merge-accumulated-persistence new-alist (cadr alist-stack))
(cddr alist-stack)))))
(defmacro accumulated-persistence (flg)
":Doc-Section Miscellaneous
to get statistics on which ~il[rune]s are being tried~/
~bv[]
Useful Forms:
(accumulated-persistence t) ; Activate statistics gathering.
(show-accumulated-persistence :frames) ; Display statistics ordered by
(show-accumulated-persistence :tries) ; frames built, times tried,
(show-accumulated-persistence :ratio) ; or their ratio.
(accumulated-persistence nil) ; Deactivate.
Advanced forms:
(show-accumulated-persistence :frames-s) ; The `s', `f', and `a' suffices
(show-accumulated-persistence :frames-f) ; stand for `success' (`useful'),
(show-accumulated-persistence :frames-a) ; `failure' (`useless'), and `all',
(show-accumulated-persistence :tries-s) ; respectively. The only effect of
(show-accumulated-persistence :tries-f) ; the `s' and `f' versions is to
(show-accumulated-persistence :tries-a) ; sort first by useful or useless
; applications, respectively (see
; below). The `a' versions avoid
; showing the useful/useless
; breakdown.
~ev[]~/
Generally speaking, the more ACL2 knows, the slower it runs. That is because
the search space grows with the number of alternative rules. Often, the
system tries to apply rules that you have forgotten were even there, if you
knew about them in the first place! ``Accumulated-persistence'' is a
statistic (originally developed for Nqthm) that helps you identify the rules
that are causing ACL2's search space to explode.
Accumulated persistence tracking can be turned on or off. It is generally
off. When on, the system may run perhaps 1.5 times slower than otherwise!
But some useful numbers are collected. When it is turned on, by
~bv[]
ACL2 !>(accumulated-persistence t)
~ev[]
an accumulation site is initialized and henceforth data about which rules are
being tried is accumulated into that site. That accumulated data can be
displayed with ~c[show-accumulated-persistence], as described in detail
below. When accumulated persistence is turned off, with
~c[(accumulated-persistence nil)], the accumulation site is wiped out and the
data in it is lost.
The ``accumulated persistence'' of a ~il[rune] is the number of ~il[rune]s
the system has attempted to apply (since accumulated persistence was last
activated) while the given ~il[rune] was being tried.
Consider a ~c[:]~ilc[rewrite] rule named ~ilc[rune]. For simplicity, let us
imagine that ~ilc[rune] is tried only once in the period during which
accumulated persistence is being ~il[monitor]ed. Recall that to apply a
rewrite rule we must match the left-hand side of the conclusion to some term
we are trying to rewrite, establish the hypotheses of ~ilc[rune] by
rewriting, and, if successful, then rewrite the right-hand side of the
conclusion. We say ~ilc[rune] is ``being tried'' from the time we have
matched its left-hand side to the time we have either abandoned the attempt
or finished rewriting its right-hand side. (By ``match'' we mean to include
any loop-stopper requirement; ~pl[loop-stopper].) During that period of time
other rules might be tried, e.g., to establish the hypotheses. The rules
tried while ~ilc[rune] is being tried are ``billed'' to ~ilc[rune] in the
sense that they are being considered here only because of the demands of
~ilc[rune]. Thus, if no other rules are tried during that period, the
accumulated persistence of ~ilc[rune] is ~c[1] ~-[] we ``bill'' ~ilc[rune]
once for its own application attempt. If, on the other hand, we tried ~c[10]
rules on behalf of that application of ~ilc[rune], then ~ilc[rune]'s
accumulated persistence would be ~c[11].
One way to envision accumulated persistence is to imagine that every
time a ~il[rune] is tried it is pushed onto a stack. The rules tried on
behalf of a given application of a ~il[rune] are thus pushed and popped
on the stack above that ~il[rune]. A lot of work might be done on its
behalf ~-[] the stack above the ~il[rune] grows and shrinks repeatedly as
the search continues for a way to use the ~il[rune]. All the while, the
~il[rune] itself ``persists'' in the stack, until we finish with the
attempt to apply it, at which time we pop it off. The accumulated
persistence of a ~il[rune] application is thus the number of stack frames
built while that ~il[rune] was on the stack.
Note that accumulated persistence is tallied whether or not the attempt to
apply a ~il[rune] is successful. Each of the rules tried on its behalf might
have failed and the attempt to apply the ~il[rune] might have also failed.
The ACL2 proof script would make no mention of the ~il[rune] or the rules
tried on its behalf because they did not contribute to the proof. But time
was spent pursuing the possible application of the ~il[rune] and accumulated
persistence is a measure of that time.
A high accumulated persistence might come about in two extreme ways. One is
that the rule causes a great deal of work every time it is tried. The other
is that the rule is ``cheap'' but is tried very often. We therefore keep
track of the number of times each rule is tried as well as its persistence.
The ratio between the two is the average amount of work done on behalf of the
rule each time it is tried.
When the accumulated persistence totals are displayed by the function
~c[show-accumulated-persistence] we sort them so that the most expensive
~il[rune]s are shown first. We can sort according to one of three basic
keys:
~bv[]
:frames - the number of frames built on behalf of the rune
:tries - the number of times the rune was tried
:ratio - frames built per try
~ev[]
The key simply determines the order in which the information is presented.
If no argument is supplied to ~c[show-accumulated-persistence], ~c[:frames]
is used.
The display breaks each total into ``useful'' and ``useless'' subtotals.
``Useful'' rule applications are those that are viewed as contributing to the
progress of the proof, and the rest are ``useless'' rule applications. For
example, if a ~c[:]~ilc[rewrite] rule is tried but its hypotheses are not
successfully relieved, then that rule application and all work done on behalf
of those hypotheses is ``useless'' work. In general, an attempt to apply a
~il[rune] is viewed as ``useful'' unless the attempt fails or the attempt is
on the stack (as described above) for a ~il[rune] application that ultimately
fails. A large number of ``useless'' ~c[:frames] or ~c[:tries] along with
correspondingly small ``useful'' counts may suggest ~il[rune]s to consider
disabling (~pl[disable] and ~pl[in-theory]). Thus, here is a more complete
list of the arguments that may be supplied to
~c[show-accumulated-persistence], Suffices ``s'', ``f'', and ``a'' are
intended to suggest ``success'' (``useful''), ``failure'' (``useless''), and
``all''.
~bv[]
:frames - sort by the number of frames built on behalf of the rune
:frames-s - as above, but sort by useful applications
:frames-f - as above, but sort by useless applications
:frames-a - as above, but inhibit display of ``useful'' and
``useless'' subtotals
:tries - sort by the number of times the rune was tried
:tries-s - as above, but sort by useful applications
:tries-f - as above, but sort by useless applications
:tries-a - as above, but inhibit display of ``useful'' and
``useless'' subtotals
:ratio - sort by frames built per try
:useless - show only the runes tried whose tries were all ``useless''
~ev[]
Note that a ~il[rune] with high accumulated persistence may not actually be
the ``culprit.'' For example, suppose ~c[rune1] is reported to have a
~c[:ratio] of ~c[101], meaning that on the average a hundred and one frames
were built each time ~c[rune1] was tried. Suppose ~c[rune2] has a ~c[:ratio]
of ~c[100]. It could be that the attempt to apply ~c[rune1] resulted in the
attempted application of ~c[rune2] and no other ~il[rune]. Thus, in some
sense, ~c[rune1] is ``cheap'' and ~c[rune2] is the ``culprit'' even though it
costs less than ~c[rune1].
There are other subtleties in how rune applications are tallied, documented
elsewhere: ~pl[accumulated-persistence-subtleties].
Users are encouraged to think about other meters we could install in ACL2 to
help diagnose performance problems."
`(wormhole t 'accumulated-persistence
nil
'(pprogn (f-put-global 'wormhole-output
(if ,flg
(make accp-info
:cnt-s 0
:cnt-f 0
:stack-s nil
:stack-f nil
:totals '(nil))
nil)
state)
(value :q))
:ld-prompt nil
:ld-pre-eval-filter :all
:ld-pre-eval-print nil
:ld-post-eval-print :command-conventions
:ld-evisc-tuple nil
:ld-error-triples t
:ld-error-action :error
:ld-query-control-alist nil
:ld-verbose nil))
(defdoc accumulated-persistence-subtleties
":Doc-Section accumulated-persistence
some subtle aspects of the counting done by ~ilc[accumulated-persistence]~/
In this topic we cover the overcounting of ``useful'' and of recursive
~il[rune] application attempts, and we describe how ``useless'' ~il[rune]
application attempts can actually be critical for a proof's success.~/
~em[Overcounting of ``useful'' and of recursive rune application attempts.]
Not every ~il[rune] application may be necessary for a proof's success.
Consider for example:
~bv[]
(thm (equal (car (cons a (cdr (cons b x))))
a))
~ev[]
Then ~c[show-accumulated-persistence] will tell us that ~c[:]~ilc[rewrite]
rules ~c[car-cons] and ~c[cdr-cons] each had one useful application.
However, the rule ~c[cdr-cons] is used to simplify ~c[(cdr (cons b x))] to
~c[x], and this simplification is unecessary for the proof. Indeed, the
proof succeeds even when preceded by the event:
~c[(in-theory (disable cdr-cons))]. We thus see that a ~il[rune] application
labeled as ``useful'' may be simplifying a term that is not relevant to the
proof.
As of this writing, we consider every forward-chaining rule application to be
``useful'', for simplicity of the implementation.
Next we show how recursive rule applications are overcounted. Consider the
following example.
~bv[]
(defun mem (a x)
(if (atom x)
nil
(or (equal a (car x)) (mem a (cdr x)))))
~ev[]
Now suppose we consider the sequence of theorems ~c[(mem a (list a))],
~c[(mem a (list 1 a))], ~c[(mem a (list 1 2 a))], ~c[(mem a (list 1 2 3 a))],
and so on. We will see that the ~c[:frames] reported for each increases
quadratically, even though the ~c[:tries] increases linearly; so in this case
the ~c[:tries] statistics are more appropriate. Each time the definition of
~c[mem] is applied, a new stack frame is pushed
(~pl[accumulated-persistence]), and all subsequent applications of that
definition are accumulated into the ~c[:frames] count for that stack frame.
The final ~c[:frames] count will be the sum of the counts for those
individual frames, which form a linear sequence whose sum is therefore
quadratic in the number of applications of the definition of ~c[mem].
~em[How ``useless'' attempts can be critical for a proof's success.] The
command ~c[(accumulated-persistence :useless])] will list rules that did not
contribute directly to the proof (~pl[accumulated-persistence], in particular
the discussion of ``useless'' there). However, a ``useless'' rule can on
rare occasions be critical to the success of a proof. In the following
example, we have a ``bad'' rule that can take the proof in the wrong
direction, but a ``useless'' rule does a rewrite that prevents the succesful
relieving of a hypothesis of the ``bad'' rule. In summary:
~bv[]
; Assume p0. We want to prove p1.
; Key rule:
p0 -> p1 = t
; Bad rule that could ruin the proof:
p3 -> p1 = p2
; But unfortunately, we know p3:
p0 -> p3
; Important ``useless'' rule, preventing ``bad rule'' above from firing:
p3 = p4
~ev[]
The following event captures the rules described above.
~bv[]
(encapsulate
((p0 (x) t)
(p1 (x) t)
(p2 (x) t)
(p3 (x) t)
(p4 (x) t))
(local (defun p0 (x) x))
(local (defun p1 (x) x))
(local (defun p2 (x) x))
(local (defun p3 (x) x))
(local (defun p4 (x) x))
; Key rule:
(defthm p0-implies-p1
(implies (p0 x)
(p1 x)))
; Bad rule that could ruin the proof:
(defthm p3-implies-p1-is-p2
(implies (p3 x)
(equal (p1 x) (p2 x))))
; But unfortunately, we know p3:
(defthm p0-implies-p3
(implies (p0 x)
(p3 x)))
; Important ``useless'' rule, preventing p3-implies-p1-is-p2 from firing:
(defthm p3-is-p4
(equal (p3 x) (p4 x))))
~ev[]
Now we can see that ~c[p3-is-p4] is labeled as ``useless'', by evaluating
these commands.
~bv[]
(accumulated-persistence t)
(thm (implies (p0 x) (p1 x)))
(show-accumulated-persistence)
~ev[]
If instead we first evaluate ~c[(in-theory (disable p3-is-p4))] before the
~c[thm] above, then the proof fails, even though ~c[p3-is-p4] was labeled as
``useless''!
Nevertheless, in general it is probably safe to disable rules reported as
``useless'' by ~c[(show-accumulated-persistence :useless)], and doing so may
speed up a proof considerably.
Remark. The example above suggests a surprising fact: on rare occasions, a
proof may fail when you give an ~c[:]~ilc[in-theory] hint consisting of
exactly the ~il[rune]s reported in a proof that succeeds. For, imagine a
rule R that is needed in part of the proof but is ``bad'' in a second part,
and that some other, ``useless'' rule prevents the application of R in that
second part. The example above suggests that disabling this ``useless'' rule
can allow the second application of R, thus preventing the proof.")
; Expected to be logic mode in ACL2 3.3:
(defun merge-lexorder (l1 l2 acc)
(declare (xargs :guard (and (true-listp l1)
(true-listp l2)
(true-listp acc))
:measure (+ (len l1) (len l2))))
(cond ((endp l1) (revappend acc l2))
((endp l2) (revappend acc l1))
((lexorder (car l1) (car l2))
(merge-lexorder (cdr l1) l2 (cons (car l1) acc)))
(t
(merge-lexorder l1 (cdr l2) (cons (car l2) acc)))))
(local
(defthm <=-len-evens
(<= (len (evens l))
(len l))
:rule-classes :linear
:hints (("Goal" :induct (evens l)))))
(local
(defthm <-len-evens
(implies (consp (cdr l))
(< (len (evens l))
(len l)))
:rule-classes :linear))
(defthm true-listp-merge-sort-lexorder
(implies (and (true-listp l1)
(true-listp l2))
(true-listp (merge-lexorder l1 l2 acc)))
:rule-classes :type-prescription)
; Expected to be logic mode in ACL2 3.3:
(defun merge-sort-lexorder (l)
(declare (xargs :guard (true-listp l)
:measure (len l)))
(cond ((endp (cdr l)) l)
(t (merge-lexorder (merge-sort-lexorder (evens l))
(merge-sort-lexorder (odds l))
nil))))
(defconst *accp-separator*
" --------------------------------~%")
(defun show-accumulated-persistence-phrase0 (entry key)
(let* ((rune (access accp-entry entry :rune))
(n-s (access accp-entry entry :n-s))
(n-f (access accp-entry entry :n-f))
(n (+ n-s n-f))
(ap-s (access accp-entry entry :ap-s))
(ap-f (access accp-entry entry :ap-f))
(ap (+ ap-s ap-f)))
(let ((main-msg
(msg "~c0 ~c1 (~c2.~f3~f4) ~y5"
(cons ap 10)
(cons n 8)
(cons (floor ap n) 5)
(mod (floor (* 10 ap) n) 10)
(mod (floor (* 100 ap) n) 10)
rune)))
(case key
((:useless :ratio-a :frames-a :tries-a)
(list main-msg))
(otherwise
(list main-msg
(msg "~c0 ~c1 [useful]~%"
(cons ap-s 10)
(cons n-s 8))
(msg "~c0 ~c1 [useless]~%"
(cons ap-f 10)
(cons n-f 8))
*accp-separator*))))))
(defun show-accumulated-persistence-phrase1 (key alist acc)
; Alist has element of the form (x . accp-entry), where x is the key upon which
; we sorted.
(cond ((null alist) acc)
(t (show-accumulated-persistence-phrase1
key
(cdr alist)
(if (and (eq key :useless)
(not (eql (access accp-entry (cdr (car alist))
:ap-s)
0)))
acc
(append (show-accumulated-persistence-phrase0 (cdr (car alist))
key)
acc))))))
(defun show-accumulated-persistence-phrase2 (key alist)
(cond ((null alist) nil)
(t (cons (cons (let* ((ap-s (access accp-entry (car alist) :ap-s))
(ap-f (access accp-entry (car alist) :ap-f))
(ap (+ ap-s ap-f))
(n-s (access accp-entry (car alist) :n-s))
(n-f (access accp-entry (car alist) :n-f))
(n (+ n-s n-f)))
(case key
((:frames :frames-a) (list* ap ap-s n n-s))
(:frames-s (list* ap-s ap n-s n))
(:frames-f (list* ap-f ap n-f n))
((:tries :tries-a) (list* n n-s ap ap-s))
(:tries-s (list* n-s n ap-s ap))
(:tries-f (list* n-f n ap-f ap))
(:useless (cons ap n))
(otherwise (/ ap n))))
(car alist))
(show-accumulated-persistence-phrase2 key (cdr alist))))))
(defun show-accumulated-persistence-phrase (key accp-info)
; Alist is the accumulated totals alist from the wormhole-output of the
; 'accumulated-persistence wormhole. Each element is of the form (rune n . ap)
; and we sort them into descending order on the specified key. Key should be
; one of
; :frames - sort on the number of frames built on behalf of the rune
; :tries - sort on the number of times the rune was tried
; :ratio - sort on frames/calls
(let ((totals (access accp-info accp-info :totals)))
(assert$
(true-listp totals)
(cond
((null totals)
(msg "There is no accumulated persistence to show. Evaluate ~x0 to ~
activate gathering of accumulated-persistence statistics.~|"
'(accumulated-persistence t)))
(t (let ((main-phrase
(list "" "~@*" "~@*" "~@*"
(show-accumulated-persistence-phrase1
key
(merge-sort-lexorder
(show-accumulated-persistence-phrase2
key (car (last totals))))
nil))))
(cond ((null (cdr totals))
(msg "Accumulated Persistence (~x0 :tries useful, ~x1 ~
:tries not useful)~% :frames :tries ~
:ratio rune~%~@2~*3"
(access accp-info accp-info :cnt-s)
(access accp-info accp-info :cnt-f)
*accp-separator*
main-phrase))
(t
(msg "Accumulated Persistence~%(Incomplete: ~x0 rule ~
attempts not considered below.)~% :frames ~
:tries :ratio rune~%~@1~*2"
(- (+ (access accp-info accp-info
:cnt-s)
(access accp-info accp-info
:cnt-f))
(+ (car (last (access accp-info accp-info
:stack-s)))
(car (last (access accp-info accp-info
:stack-f)))))
*accp-separator*
main-phrase)))))))))
(defmacro show-accumulated-persistence (&optional (sortkey ':frames))
(declare (xargs :guard (member-eq sortkey '(:ratio
:frames :frames-s :frames-f :frames-a
:tries :tries-s :tries-f :tries-a
:useless))))
`(wormhole t 'accumulated-persistence
,sortkey
'(pprogn
(io? temporary nil state
nil
(fms "~@0"
(list (cons #\0
(show-accumulated-persistence-phrase
(f-get-global 'wormhole-input state)
(f-get-global 'wormhole-output state))))
*standard-co*
state nil))
(value :q))
:ld-prompt nil
:ld-pre-eval-filter :all
:ld-pre-eval-print nil
:ld-post-eval-print :command-conventions
:ld-evisc-tuple nil
:ld-error-triples t
:ld-error-action :error
:ld-query-control-alist nil
:ld-verbose nil))
(defun push-accp ()
(assign-wormhole-output
wormhole-output
'accumulated-persistence
nil
'(let ((info (f-get-global 'wormhole-output state)))
(change accp-info info
:stack-s (cons (access accp-info info :cnt-s)
(access accp-info info :stack-s))
:stack-f (cons (access accp-info info :cnt-f)
(access accp-info info :stack-f))
:totals (cons nil
(access accp-info info :totals))))))
(defun pop-accp (rune success-p)
; Warning: Keep the two branches below in sync.
(if success-p
(assign-wormhole-output
wormhole-output
'accumulated-persistence
rune
'(let* ((rune (f-get-global 'wormhole-input state))
(info (f-get-global 'wormhole-output state))
(new-cnt-s (1+ (access accp-info info :cnt-s))))
(change accp-info info
:cnt-s new-cnt-s
:stack-s (cdr (access accp-info info :stack-s))
:stack-f (cdr (access accp-info info :stack-f))
:totals (add-accumulated-persistence
rune
t ; ,success-p
(- new-cnt-s
(car (access accp-info info :stack-s)))
(- (access accp-info info :cnt-f)
(car (access accp-info info :stack-f)))
(access accp-info info :totals)))))
(assign-wormhole-output
wormhole-output
'accumulated-persistence
rune
'(let* ((rune (f-get-global 'wormhole-input state))
(info (f-get-global 'wormhole-output state))
(new-cnt-f (1+ (access accp-info info :cnt-f))))
(change accp-info info
:cnt-f new-cnt-f
:stack-s (cdr (access accp-info info :stack-s))
:stack-f (cdr (access accp-info info :stack-f))
:totals (add-accumulated-persistence
rune
nil ; ,success-p
(- (access accp-info info :cnt-s)
(car (access accp-info info :stack-s)))
(- new-cnt-f
(car (access accp-info info :stack-f)))
(access accp-info info :totals)))))))
(defmacro with-accumulated-persistence (rune vars success-p body)
`(let ((with-accumulated-persistence-rune ,rune))
(prog2$
(push-accp)
,(cond ((and (true-listp vars)
(= (length vars) 1))
`(let ((,(car vars)
(check-vars-not-free
(with-accumulated-persistence-rune)
,body)))
(prog2$
(pop-accp with-accumulated-persistence-rune
(check-vars-not-free
(with-accumulated-persistence-rune)
,success-p))
,(car vars))))
(t `(mv-let ,vars
(check-vars-not-free
(with-accumulated-persistence-rune)
,body)
(prog2$
(pop-accp with-accumulated-persistence-rune
(check-vars-not-free
(with-accumulated-persistence-rune)
,success-p))
(mv ,@vars))))))))
(defun type-set-with-rule (tp term force-flg dwp type-alist ancestors ens w ttree
pot-lst pt)
; We apply the type-prescription, tp, to term, if possible, and return a
; type-set, an extended type-alist and a ttree. If the rule is inapplicable,
; the type-set is *ts-unknown* and the ttree is unchanged. Recall that
; type-set treats its ttree argument as an accumulator and we are obliged to
; return an extension of the input ttree.
; Note that the specification of this function is that if we were to take the
; resulting type-alist and cons the input ttree on to each ttree in that
; type-alist, the resulting type-alist would be "appropriate". In particular,
; we don't put ttree into the type-alist, but instead we assume that our caller
; will compensate appropriately.
(cond
((enabled-numep (access type-prescription tp :nume) ens)
(mv-let
(unify-ans unify-subst)
(one-way-unify (access type-prescription tp :term)
term)
(cond
(unify-ans
(with-accumulated-persistence
(access type-prescription tp :rune)
(ts type-alist-out ttree-out)
(not (ts= *ts-unknown* ts))
(let* ((hyps (access type-prescription tp :hyps))
(type-alist
(cond
((null hyps) type-alist)
(t (extend-type-alist-with-bindings unify-subst
force-flg
dwp
type-alist
ancestors
ens w
; We lie here by passing in the nil tag tree, so that we can avoid
; contaminating the resulting type-alist with a copy of ttree. We'll make sure
; that ttree gets into the answer returned by type-alist-with-rules, which is
; the only function that calls type-set-with-rule.
nil
pot-lst pt)))))
(mv-let
(relieve-hyps-ans type-alist ttree)
(type-set-relieve-hyps (access type-prescription tp :rune)
term
hyps
force-flg dwp
unify-subst
type-alist
ancestors
ens w
; We pass in nil here to avoid contaminating the type-alist returned by this
; call of type-set-relieve-hyps.
nil
ttree
pot-lst pt)
(cond
(relieve-hyps-ans
(type-set-with-rule1 unify-subst
(access type-prescription tp :vars)
force-flg
dwp
type-alist ancestors ens w
(access type-prescription tp :basic-ts)
(push-lemma
(access type-prescription tp :rune)
ttree)
pot-lst pt))
(t (mv *ts-unknown* type-alist ttree)))))))
(t (mv *ts-unknown* type-alist ttree)))))
(t (mv *ts-unknown* type-alist ttree))))
(remove-untouchable coerce-state-to-object t)
(defun rewrite-with-lemma (term lemma ; &extra formals
rdepth
type-alist obj geneqv wrld state
fnstack ancestors
backchain-limit
simplify-clause-pot-lst rcnst gstack
ttree)
; The three values returned by this function are: t or nil indicating whether
; lemma was used to rewrite term, the rewritten version of term, and the final
; version of ttree. This is a No-Change Loser.
(declare (type (unsigned-byte 29) rdepth))
(let ((gstack (push-gframe 'rewrite-with-lemma nil term lemma))
(rdepth (adjust-rdepth rdepth)))
(cond ((zero-depthp rdepth)
(rdepth-error
(mv nil term ttree)))
((f-big-clock-negative-p state)
(mv nil term ttree))
((eq (access rewrite-rule lemma :subclass) 'meta)
; See the Essay on Correctness of Meta Reasoning, above, and :doc meta.
(cond
((geneqv-refinementp (access rewrite-rule lemma :equiv)
geneqv
wrld)
; We assume that the meta function has defun-mode :logic. How could it
; be :program if we proved it correct?
; Metafunctions come in two flavors. Vanilla metafunctions take just
; one arg, the term to be rewritten. Extended metafunctions take
; three args. We cons up the args here and use this list of args
; twice below, once to eval the metafunction and once to eval the hyp
; fn. The :rhs of the rewrite-rule is the special flag 'extended
; if we are in the extended case; otherwise, :rhs is nil. We must
; manufacture a context in the former case.
(let ((args
(cond
((eq (access rewrite-rule lemma :rhs)
'extended)
(list term
(make metafunction-context
:rdepth rdepth
:type-alist type-alist
:obj obj
:geneqv geneqv
:wrld wrld
:fnstack fnstack
:ancestors ancestors
:backchain-limit backchain-limit
:simplify-clause-pot-lst
simplify-clause-pot-lst
:rcnst rcnst
:gstack gstack
:ttree ttree)
(coerce-state-to-object state)))
(t (list term))))
(rune (access rewrite-rule lemma :rune)))
(with-accumulated-persistence
rune
(flg term ttree)
flg
(mv-let
(erp val latches)
(pstk
(ev-fncall-meta (access rewrite-rule lemma :lhs)
args
(f-decrement-big-clock state)))
(declare (ignore latches))
(cond
(erp
(mv nil term ttree))
((equal term val)
(mv nil term ttree))
((termp val wrld)
(let ((hyp-fn (access rewrite-rule lemma :hyps)))
(mv-let
(erp evaled-hyp latches)
(if (eq hyp-fn nil)
(mv nil *t* nil)
(pstk
(ev-fncall-meta hyp-fn
args
(f-decrement-big-clock state))))
(declare (ignore latches))
(cond
(erp
(mv nil term ttree))
((termp evaled-hyp wrld)
(let* ((vars (all-vars term))
(hyps (flatten-ands-in-lit
; Note: The sublis-var below normalizes the explicit constant
; constructors in evaled-hyp, e.g., (cons '1 '2) becomes '(1 . 2).
(sublis-var nil evaled-hyp)))
(rule-backchain-limit
(access rewrite-rule lemma
:backchain-limit-lst))
(bad-synp-hyp-msg
(bad-synp-hyp-msg hyps vars nil wrld)))
(cond
(bad-synp-hyp-msg
(mv (er hard 'rewrite-with-lemma
"The hypothesis metafunction ~x0, when ~
applied to the input term ~x1, produced a ~
term whose use of synp is illegal because ~
~@2"
hyp-fn
term
bad-synp-hyp-msg)
term ttree))
(t
(mv-let
(relieve-hyps-ans failure-reason unify-subst ttree1)
(rewrite-entry (relieve-hyps
; The next argument of relieve-hyps is a rune on which to "blame" a
; possible force. We could blame such a force on a lot of things, but
; we'll blame it on the metarule and the term that it's applied to.
rune
term
hyps
(and rule-backchain-limit
(assert$
(natp rule-backchain-limit)
(make-list
(length hyps)
:initial-element
rule-backchain-limit)))
; The meta function has rewritten term to val and has generated a
; hypothesis called evaled-hyp. Now ignore the metafunction and just
; imagine that we have a rewrite rule (implies evaled-hyp (equiv term
; val)). The unifying substitution just maps the vars of term to
; themselves. There may be additional vars in both evaled-hyp and in
; val. But they are free at the time we do this relieve-hyps.
(pairlis$ vars vars)
nil ; allp=nil for meta rules
)
:obj nil
:geneqv nil)
; If relieve hyps succeeds we get back a unifying substitution that extends
; the identity substitution above. This substitution might bind free vars
; in the evaled-hyp.
; Why are we ignoring failure-reason? Do we need to be calling one of the
; brkpt functions? No, because we don't break on meta rules. But perhaps we
; should consider allowing breaks on meta rules.
(declare (ignore failure-reason))
(cond
(relieve-hyps-ans
(mv-let
(rewritten-rhs ttree)
(rewrite-entry (rewrite
; Note: The sublis-var below normalizes the explicit constant
; constructors in val, e.g., (cons '1 '2) becomes '(1 . 2).
(sublis-var nil val)
; At one point we ignored the unify-subst constructed above and used a
; nil here. That was unsound if val involved free vars bound by the
; relief of the evaled-hyp. We must rewrite val under the extended
; substitution. Often that is just the identity substitution.
unify-subst
'meta)
:ttree
; Should we be pushing executable counterparts into ttrees when we applying
; metafunctions on behalf of meta rules? NO: We should only do that if the
; meta-rule's use is sensitive to whether or not they're enabled, and it's not
; -- all that matters is if the rule itself is enabled.
(push-lemma
(geneqv-refinementp
(access rewrite-rule lemma :equiv)
geneqv
wrld)
(push-lemma rune ttree1)))
(mv t rewritten-rhs ttree)))
(t (mv nil term ttree))))))))
(t (mv (er hard 'rewrite-with-lemma
"The hypothesis function ~x0 produced the ~
non-termp ~x1 on the input term ~x2. Our ~
implementation requires that ~x0 produce a ~
term."
hyp-fn
evaled-hyp
term
(access rewrite-rule lemma :lhs))
term ttree))))))
(t (mv (er hard 'rewrite-with-lemma
"The metafunction ~x0 produced the non-termp ~x1 ~
on the input term ~x2. The proof of the ~
correctness of ~x0 establishes that the ~
quotations of these two s-expressions have the ~
same value, but our implementation additionally ~
requires that ~x0 produce a term."
(access rewrite-rule lemma :lhs)
val
term)
term ttree)))))))
(t (mv nil term ttree))))
((not (geneqv-refinementp (access rewrite-rule lemma :equiv)
geneqv
wrld))
(mv nil term ttree))
((eq (access rewrite-rule lemma :subclass) 'definition)
(mv-let (rewritten-term ttree)
(rewrite-entry (rewrite-fncall lemma term))
(mv (not (equal term rewritten-term)) rewritten-term ttree)))
((and (or (null (access rewrite-rule lemma :hyps))
(not (eq obj t))
(not (equal (access rewrite-rule lemma :rhs) *nil*)))
(or (flambdap (ffn-symb term)) ; hence not on fnstack
(not (being-openedp (ffn-symb term) fnstack
(recursivep (ffn-symb term) wrld)))
(not (ffnnamep (ffn-symb term)
(access rewrite-rule lemma :rhs)))))
(let ((lhs (access rewrite-rule lemma :lhs))
(rune (access rewrite-rule lemma :rune)))
(mv-let (unify-ans unify-subst)
(one-way-unify-restrictions
lhs
term
(cdr (assoc-equal
rune
(access rewrite-constant rcnst
:restrictions-alist))))
(cond
((and unify-ans
(null (brkpt1 lemma term unify-subst
type-alist ancestors
ttree
gstack state)))
(cond
((null (loop-stopperp
(access rewrite-rule lemma :heuristic-info)
unify-subst
wrld))
(prog2$
(brkpt2 nil 'loop-stopper
unify-subst gstack nil nil
rcnst state)
(mv nil term ttree)))
(t
(with-accumulated-persistence
rune
(flg term ttree)
flg
(mv-let
(relieve-hyps-ans failure-reason unify-subst ttree)
(rewrite-entry (relieve-hyps
rune
term
(access rewrite-rule lemma :hyps)
(access rewrite-rule lemma
:backchain-limit-lst)
unify-subst
(not (oncep (access rewrite-constant
rcnst
:oncep-override)
(access rewrite-rule
lemma
:match-free)
rune
(access rewrite-rule
lemma
:nume))))
:obj nil
:geneqv nil)
(cond
(relieve-hyps-ans
(mv-let
(rewritten-rhs ttree)
(rewrite-entry
(rewrite
(access rewrite-rule lemma :rhs)
unify-subst
'rhs))
(prog2$
(brkpt2 t nil unify-subst gstack rewritten-rhs
ttree rcnst state)
(mv t rewritten-rhs
(push-lemma (geneqv-refinementp
(access rewrite-rule lemma :equiv)
geneqv
wrld)
(push-lemma
rune
ttree))))))
(t (prog2$
(brkpt2 nil failure-reason
unify-subst gstack nil nil
rcnst state)
(mv nil term ttree)))))))))
(t (mv nil term ttree))))))
(t (mv nil term ttree)))))
(defun rewrite-fncall (rule term ; &extra formals
rdepth
type-alist obj geneqv wrld state fnstack ancestors
backchain-limit
simplify-clause-pot-lst rcnst gstack ttree)
; Rule is a :REWRITE rule of subclass DEFINITION or else it is nil.
; Rule is nil iff term is a lambda application. The two values
; returned by this function are the usual rewrite pair: the (possibly)
; rewritten term and the new ttree. We assume rule is enabled.
; Term is of the form (fn . args).
; Nqthm Discrepancy: In nqthm, the caller of rewrite-fncall,
; rewrite-with-lemmas, would ask whether the result was different from term and
; whether it contained rewriteable calls. If so, it called the rewriter on the
; result. We have changed that here so that rewrite-fncall, in the case that
; it is returning the expanded body, asks about rewriteable calls and possibly
; calls rewrite again. In the implementation below we ask about rewriteable
; calls only for recursively defined fns. The old code asked the question on
; all expansions. It is possible the old code sometimes found a rewriteable
; call of a non-recursive fn in the expansion of that fn's body because of uses
; of that fn in the arguments. So this is a possible difference between ACL2
; and nqthm, although we have no reason to believe it is significant and we do
; it only for recursive fns simply because the non-recursive case seems
; unlikely.
(declare (type (unsigned-byte 29) rdepth))
(let* ((fn (ffn-symb term))
(args (fargs term))
(body (if (null rule)
(or (lambda-body fn)
(er hard 'rewrite-fncall
"We had thought that a lambda function symbol ~
always has a non-nil lambda-body, but the ~
following lambda does not: ~x0"
fn))
(or (access rewrite-rule rule :rhs)
"We had thought that a rewrite-rule always has a non-nil ~
:rhs, but the following rewrite rule does not: ~x0")))
(recursivep (and rule ; it's a don't-care if (flambdap fn)
(car (access rewrite-rule rule :heuristic-info)))))
(cond ((f-big-clock-negative-p state)
(mv term ttree))
((and (not (flambdap fn))
(or (being-openedp fn fnstack recursivep)
(fnstack-term-member term fnstack)))
(rewrite-solidify term type-alist obj geneqv
(access rewrite-constant rcnst
:current-enabled-structure)
wrld ttree
simplify-clause-pot-lst
(access rewrite-constant rcnst :pt)))
((null rule) ; i.e., (flambdap fn)
(mv-let
(rewritten-body ttree1)
(rewrite-entry (rewrite body
(pairlis$ (lambda-formals fn) args)
'body)
:fnstack fnstack)
; Observe that we do not put the lambda-expression onto the fnstack.
; We act just as though we were rewriting a term under a substitution.
; But we do decide on heuristic grounds whether to keep the expansion.
; See the handling of non-recursive functions below for some comments
; relating to the too-many-ifs code.
; Note: If the handling of lambda-applications is altered, consider
; their handling in both rewrite-fncallp (where we take advantage of
; the knowledge that lambda-expressions will not occur in rewritten
; bodies unless the user has explicitly prevented us from opening
; them) and contains-rewriteable-callp.
(cond
((and (not (recursive-fn-on-fnstackp fnstack))
(too-many-ifs args rewritten-body))
(rewrite-solidify term type-alist obj geneqv
(access rewrite-constant rcnst
:current-enabled-structure)
wrld ttree
simplify-clause-pot-lst
(access rewrite-constant rcnst :pt)))
(t (mv rewritten-body ttree1)))))
(t
(let* ((new-fnstack (cons (or recursivep fn) fnstack))
(rune (access rewrite-rule rule :rune)))
(mv-let
(unify-ans unify-subst)
(one-way-unify-restrictions
(access rewrite-rule rule :lhs)
term
(cdr (assoc-equal
rune
(access rewrite-constant rcnst
:restrictions-alist))))
(cond
((and unify-ans
(null (brkpt1 rule term unify-subst type-alist ancestors
ttree gstack state)))
(with-accumulated-persistence
(access rewrite-rule rule :rune)
(term-out ttree)
(not (eq term term-out)) ; mis-guarded use of eq
(mv-let
(relieve-hyps-ans failure-reason unify-subst ttree1)
(cond
((and (eq fn (base-symbol rune))
; There may be alternative definitions of fn. "The" definition is the one
; whose rune is of the form (:DEFINITION fn); its hyps is nil, at least in the
; standard case; but:
#+:non-standard-analysis
; In the non-standard case, we may be attempting to open up a call of a
; function defined by defun-std. Hence, there may be one or more hypotheses.
(not (access rewrite-rule rule :hyps)))
(mv t nil unify-subst ttree))
(t (rewrite-entry
(relieve-hyps rune term
(access rewrite-rule rule :hyps)
nil ; backchain-limit-lst
unify-subst
nil ; allp=nil for definitions
)
:obj nil
:geneqv nil)))
(cond
(relieve-hyps-ans
(mv-let
(rewritten-body ttree1)
(rewrite-entry (rewrite body unify-subst 'body)
:fnstack new-fnstack
:ttree ttree1)
; Again, we use ttree1 to accumulate the successful rewrites and we'll
; return it in our answer if we like our answer.
(cond
((null recursivep)
; We are dealing with a nonrecursive fn. If we are at the top-level of the
; clause but the expanded body has too many IFs in it compared to the number
; in the args, we do not use the expanded body. We know the IFs in
; the args will be clausified out soon and then this will be permitted to
; open.
(cond
((and (not (recursive-fn-on-fnstackp fnstack))
(too-many-ifs args rewritten-body))
(prog2$
(brkpt2 nil 'too-many-ifs unify-subst gstack
rewritten-body ttree1 rcnst state)
(rewrite-solidify term type-alist obj geneqv
(access rewrite-constant rcnst
:current-enabled-structure)
wrld ttree
simplify-clause-pot-lst
(access rewrite-constant rcnst :pt))))
(t (prog2$
(brkpt2 t nil unify-subst gstack
rewritten-body ttree1 rcnst state)
(mv rewritten-body
(push-lemma rune ttree1))))))
((rewrite-fncallp
term rewritten-body
(if (cdr recursivep) recursivep nil)
(access rewrite-constant rcnst
:top-clause)
(access rewrite-constant rcnst
:current-clause)
(cdr (access rewrite-rule rule :heuristic-info)))
(cond
; Once upon a time, before we were heavily involved with ACL2 proofs, we had
; the following code here. Roughly speaking this code forced recursive
; functions to open one step at a time if they introduced any IFs.
; ((ffnnamep 'if rewritten-body)
; Nqthm Discrepancy: This clause is new to ACL2. Nqthm always rewrote the
; rewritten body if it contained rewriteable calls. This allows Nqthm to open
; up (member x '(a b c d e)) to a 5-way case split in "one" apparent rewrite.
; In an experiment I have added the proviso above, which avoids rewriting the
; rewritten body if it contains an IF. This effectively slows down the opening
; of member, forcing the whole theorem back through the simplifier on each
; opening. Eventually it will open completely, even under this rule. The
; thought, though, is that often the case splits introduced by such openings
; seems to be irrelevant. Under this new rule, (length (list a b c d e)) will
; expand in one step to '5, but the member expression above will expand more
; slowly because the expansion introduces a case split. An experiment was done
; with Nqthm-1992 in which this change was introduced and examples/basic/
; proveall.events was replayed without any trouble and with no apparent
; performance change. There are undoubtedly example files where this change
; will slow things down. But it was motivated by an example in which it speeds
; things up by a factor of 10 because the opening is totally irrelevant to the
; proof. The problem -- which was illustrated in the guard proofs for the
; function ascii-code-lst in the nqthm.lisp events -- is that (member x
; *standard-chars*) opens into a 96-way case split in a situation in which it
; could as well have been disabled. This happens more in ACL2 than in Nqthm
; because of the presence of defconsts which permit big constants to be fed
; to recursive functions. It is not clear whether this change is an improvement
; or not.
; (prog2$
; (brkpt2 t nil unify-subst gstack rewritten-body
; ttree1 rcnst state)
; (mv rewritten-body
; (push-lemma rune ttree1))))
; With further experience, I've decided it is clear that this change is not an
; improvement! I really like Nqthm's behavior. The example cited above is
; still a problem. In particular,
#|
(defun ascii-code-lst (lst)
; This function converts a standard char list into the list of their
; ascii codes, terminated by a 0.
(declare (xargs :guard (standard-char-listp lst)
:hints (("Goal" :in-theory (disable member)))
:guard-hints (("Goal" :in-theory (disable member)))))
(if (null lst)
0
(cons (ascii-code (car lst))
(ascii-code-lst (cdr lst)))))
|#
; takes forever unless you give the two disable hints shown above.
((contains-rewriteable-callp
fn rewritten-body
(if (cdr recursivep)
recursivep
nil)
(access rewrite-constant
rcnst :terms-to-be-ignored-by-rewrite))
; Ok, we are prepared to rewrite the once rewritten body. But beware! There
; is an infinite loop lurking here. It can be broken by using :fnstack
; new-fnstack. While the loop can be broken by using new-fnstack, that
; approach has a bad side-effect: (member x '(a b c)) is not runout. It opens
; to (if (equal x 'a) (member x '(b c))) and because new-fnstack mentions
; member, we don't expand the inner call. See the comment in
; fnstack-term-member for a discussion of loop avoidance (which involved code
; that was here before Version_2.9).
(mv-let (rewritten-body ttree2)
(rewrite-entry (rewrite rewritten-body nil
'rewritten-body)
:fnstack
; See the reference to fnstack in the comment above.
(cons (cons :TERM term)
fnstack)
:ttree (push-lemma rune
ttree1))
(prog2$
(brkpt2 t nil unify-subst gstack
rewritten-body ttree2 rcnst state)
(mv rewritten-body ttree2))))
(t
(prog2$
(brkpt2 t nil unify-subst gstack rewritten-body
ttree1 rcnst state)
(mv rewritten-body
(push-lemma rune ttree1))))))
(t (prog2$
(brkpt2 nil 'rewrite-fncallp unify-subst gstack
rewritten-body ttree1 rcnst state)
(rewrite-solidify term type-alist obj geneqv
(access rewrite-constant rcnst
:current-enabled-structure)
wrld ttree
simplify-clause-pot-lst
(access rewrite-constant rcnst :pt)))))))
(t (prog2$
(brkpt2 nil failure-reason unify-subst gstack nil
nil rcnst state)
(rewrite-solidify term type-alist obj geneqv
(access rewrite-constant rcnst
:current-enabled-structure)
wrld ttree
simplify-clause-pot-lst
(access rewrite-constant rcnst :pt))))))))
(t (rewrite-solidify term type-alist obj geneqv
(access rewrite-constant rcnst
:current-enabled-structure)
wrld ttree
simplify-clause-pot-lst
(access rewrite-constant rcnst :pt))))))))))
(defun add-linear-lemma (term lemma ; &extra formals
rdepth
type-alist obj geneqv wrld state fnstack ancestors
backchain-limit
simplify-clause-pot-lst rcnst gstack ttree)
; We investigate the application of lemma to term and the
; simplify-clause-pot-lst. If term unifies with the max-term of lemma and we
; can relieve the hypotheses, we add the polynomial produced from lemma's
; conclusion to the pot-lst. We return two values. The first is the standard
; contradictionp. The second is a possibly modified simplify-clause-pot-lst.
; PATCH: We use a new field in the linear pots to catch potential loops.
; Loop-stopper-value is initially 0 in all the linear pots. Let value be the
; loop-stopper-value associated with term in simplify-clause-pot-lst. When we
; return a new linear-pot-list, we check to see if there are any new pots. Let
; pot be such a new pot. If the largest var in pot is term order greater than
; term, we set the loop-stopper-value of pot to value + 1. Otherwise, we set
; it to value.
; Now, before we actually add any polys to simplify-clause-pot-lst, we call
; no-new-and-ugly-linear-varsp on the list of polys to be added. This function
; (among other things) checks whether the new vars would have a
; loop-stopper-value which exceeds *max-linear-pot-loop-stopper-value*.
(declare (ignore obj geneqv ttree)
(type (unsigned-byte 29) rdepth))
; Convention: It is our convention to pass nils into ignored &extra formals.
; Do not change the (ignore ...) declaration above without looking at the
; callers. That is, if you change this function so that it uses the formals
; declared ignored above, you are making a mistake because all callers of this
; function pass nils into them.
(mv-let (unify-ans unify-subst)
(one-way-unify (access linear-lemma lemma :max-term)
term)
(cond
((f-big-clock-negative-p state)
(mv nil simplify-clause-pot-lst))
(unify-ans
(with-accumulated-persistence
(access linear-lemma lemma :rune)
(contradictionp pot-lst)
(or contradictionp
(not (eq pot-lst simplify-clause-pot-lst))) ; mis-guarded use of eq
(mv-let
(relieve-hyps-ans failure-reason unify-subst ttree1)
(let ((rune (access linear-lemma lemma :rune)))
(rewrite-entry (relieve-hyps rune
term
(access linear-lemma lemma :hyps)
(access linear-lemma lemma
:backchain-limit-lst)
unify-subst
(not (oncep (access rewrite-constant
rcnst
:oncep-override)
(access linear-lemma lemma
:match-free)
rune
(access linear-lemma lemma
:nume))))
:obj nil
:geneqv nil
:ttree nil))
(declare (ignore failure-reason))
(cond
(relieve-hyps-ans
(mv-let
(rewritten-concl ttree2)
(rewrite-entry (rewrite-linear-term
(access linear-lemma lemma :concl)
unify-subst)
:obj nil
:geneqv nil
:ttree ttree1)
; Previous to Version_2.7, we just went ahead and used the result of
; (linearize rewritten-concl ...). This had long been known to be
; problematic (see the comments in linearize1 beginning ``This is a
; strange one.'') but nothing had been done about it. Then Eric Smith
; sent the following example to us and wanted to know what was going
; wrong.
#|
(defstub bitn (x n) t) ; extract bit n of x
(skip-proofs
(defthm bitn-non-negative-integer
(and (integerp (bitn x n))
(<= 0 (bitn x n)))
:rule-classes (:rewrite :type-prescription)))
(skip-proofs
(defthm bits-upper-bound-linear
(< (bits x i j) (expt 2 (+ i 1 (- j))))
:rule-classes ((:linear :trigger-terms ((bits x i j))))))
;goes through (using the two :linear rules above)
(thm
(< (+ (BITN x 32)
(BITN x 58))
2))
;the problem rule.
(skip-proofs
(defthm bitn-known-not-0-replace-with-1
(implies (not (equal (bitn x n) 0))
(equal (bitn x n)
1))))
;same thm; now fails --- the rule above causes linear arithmetic to fail.
(thm
(< (+ (BITN x 32)
(BITN x 58))
2))
|#
; If one uses the following trace and replays the above script, one
; can see what was happening (In a nutshell, ACL2 rewrites the (BITN B
; Z) in the instantiated conclusion of bitn-upper-bound-linear, (<=
; (BITN B Z) 1), to 1 yielding (<= 1 1), which is trivially true but
; not very useful.
#|
(defun show-type-alist (type-alist)
(cond ((endp type-alist) nil)
(t (cons (list (car (car type-alist))
(decode-type-set (cadr (car type-alist))))
(show-type-alist (cdr type-alist))))))
SHOW-TYPE-ALIST
ACL2(3): (trace (add-polys
:entry (list (list 'new-polys (show-poly-lst (nth 0 arglist)))
(list 'pot-lst (show-pot-lst (nth 1 arglist)))
(list 'type-alist (show-type-alist (nth 3 arglist))))
:exit (list (list 'contradictionp (nth 0 values))
(list 'new-pot-lst (show-pot-lst (nth 1 values)))))
(add-linear-lemma
:entry (list (list 'term (nth 0 arglist))
(list 'lemma (nth 1 arglist)))
:exit (list (list 'contradictionp (nth 0 values))
(list 'new-pot-lst (show-pot-lst (nth 1 values)))))
(rewrite-linear-term
:entry (list (list 'term (sequential-subst-var-term (nth 1 arglist)
(nth 0 arglist))))
:exit (list (list 'rewritten-term (nth 0 values))
(list 'ttree (nth 1 arglist)))))
(REWRITE-LINEAR-TERM ACL2_*1*_ACL2::REWRITE-LINEAR-TERM ADD-LINEAR-LEMMA
ACL2_*1*_ACL2::ADD-LINEAR-LEMMA ADD-POLYS
ACL2_*1*_ACL2::ADD-POLYS)
|#
; The best solution would probably be to not rewrite the instantiated
; trigger term in rewrite-linear-term, but that has its own problems
; and is much more work to implement. By just reverting to the
; un-rewritten concl we catch the ``obvious'' cases such as
; illustrated above. Note that the un-rewritten concl may also
; linearize to nil, but a regression test using the books distributed
; with ACL2 actually shows a slight improvement in speed (about a
; minute and a half, out of 158 and a half minutes), so we conclude
; that this is not a problem in practice.
; We thank Robert Krug for providing this improvement.
(let* ((force-flg (ok-to-force rcnst))
(temp-lst (linearize rewritten-concl
t
type-alist
(access rewrite-constant rcnst
:current-enabled-structure)
force-flg
wrld
(push-lemma
(access linear-lemma lemma :rune)
ttree2)
state))
(lst (or temp-lst
(linearize (sublis-var
unify-subst
(access linear-lemma lemma :concl))
t
type-alist
(access rewrite-constant rcnst
:current-enabled-structure)
force-flg
wrld
(push-lemma
(access linear-lemma lemma :rune)
ttree1)
state))))
(cond
((and (null (cdr lst))
(not (new-and-ugly-linear-varsp
(car lst)
(<= *max-linear-pot-loop-stopper-value*
(loop-stopper-value-of-var
term
simplify-clause-pot-lst))
term)))
(mv-let
(contradictionp new-pot-lst)
(add-polys (car lst)
simplify-clause-pot-lst
(access rewrite-constant rcnst :pt)
(access rewrite-constant rcnst :nonlinearp)
type-alist
(access rewrite-constant rcnst
:current-enabled-structure)
force-flg
wrld)
(cond
(contradictionp (mv contradictionp nil))
(t (mv nil
(set-loop-stopper-values
(new-vars-in-pot-lst new-pot-lst
simplify-clause-pot-lst)
new-pot-lst
term
(loop-stopper-value-of-var
term simplify-clause-pot-lst)))))))
(t (mv nil simplify-clause-pot-lst))))))
(t (mv nil simplify-clause-pot-lst))))))
(t (mv nil simplify-clause-pot-lst)))))
(defun mult-advance-fc-activation (act type-alist ens oncep-override force-flg
wrld state fcd-lst)
; Act is an fc activation. Fcd-lst is a list of all of the
; fc-derivations made so far (this pass). We try to relieve the hyps of
; act. We return two results. The first is either an activation to use
; in place of act or else is nil meaning act is being discontinued. The
; second is an extension of fcd-lst containing all the newly derived
; conclusions (as fc-derivations).
(with-accumulated-persistence
(access forward-chaining-rule
(access fc-activation act :rule)
:rune)
(act-out fcd-lst-out)
t ; wart: always marked as ``useful''
(let ((inst-hyp (access fc-activation act :inst-hyp)))
(cond
((equal inst-hyp *t*)
(mult-advance-fc-activation1
act nil type-alist ens oncep-override force-flg wrld state fcd-lst))
(t (mv-let (ts ttree)
(type-set inst-hyp force-flg nil type-alist nil ens wrld nil
nil nil)
(cond ((ts= ts *ts-nil*)
(mv nil fcd-lst))
((ts-intersectp ts *ts-nil*)
(mv (list act) fcd-lst))
(t (mult-advance-fc-activation1
act ttree type-alist ens oncep-override force-flg
wrld state fcd-lst)))))))))
(defun apply-induction-rule (rule term type-alist xterm ttree ens wrld)
; We apply the induction-rule, rule, to term, and return a possibly empty list
; of suggested inductions. The basic idea is to check that the rule is enabled
; and that the :pattern of the rule matches term. If so, we check that the
; :condition of the rule is true under the current type-alist. This check is
; heuristic only and so we indicate that the guards have been checked and we
; allow forcing. We ignore the ttree because we are making a heuristic choice
; only. If type-set says the :condition is non-nil, we fire the rule by
; instantiating the :scheme and recursively getting the suggested inductions
; for that term. Note that we are not recursively exploring the instantiated
; scheme but just getting the inductions suggested by its top-level function
; symbol.
(cond
((enabled-numep (access induction-rule rule :nume) ens)
(mv-let
(ans alist)
(one-way-unify (access induction-rule rule :pattern)
term)
(cond
(ans
(with-accumulated-persistence
(access induction-rule rule :rune)
(suggestions)
suggestions
(mv-let
(ts ttree1)
(type-set (sublis-var alist
(access induction-rule rule :condition))
t nil type-alist nil ens wrld nil
nil nil)
(declare (ignore ttree1))
(cond
((ts-intersectp *ts-nil* ts) nil)
(t (let ((term1 (sublis-var alist
(access induction-rule rule :scheme))))
(cond ((or (variablep term1)
(fquotep term1))
nil)
(t (suggested-induction-cands term1 type-alist
xterm
(push-lemma
(access induction-rule
rule
:rune)
ttree)
ens wrld)))))))))
(t nil))))
(t nil)))
(defun expand-abbreviations-with-lemma (term geneqv
fns-to-be-ignored-by-rewrite
rdepth ens wrld state ttree)
(mv-let
(wonp cr-rune lemma unify-subst)
(find-abbreviation-lemma term geneqv
(getprop (ffn-symb term) 'lemmas nil
'current-acl2-world wrld)
ens
wrld)
(cond
(wonp
(with-accumulated-persistence
(access rewrite-rule lemma :rune)
(term ttree)
t
(expand-abbreviations
(access rewrite-rule lemma :rhs)
unify-subst
geneqv
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) ens wrld state
(push-lemma cr-rune
(push-lemma (access rewrite-rule lemma :rune)
ttree)))))
(t (mv term ttree)))))
(remove-untouchable ev-fncall t)
(defun expand-abbreviations (term alist geneqv fns-to-be-ignored-by-rewrite
rdepth ens wrld state ttree)
; This function is essentially like rewrite but is more restrictive in
; its use of rules. We rewrite term/alist maintaining geneqv and
; avoiding the expansion or application of lemmas to terms whose fns
; are in fns-to-be-ignored-by-rewrite. We return a new term and a
; ttree (accumulated onto our argument) describing the rewrite. We
; only apply "abbreviations" which means we expand lambda applications
; and non-rec fns provided they do not duplicate arguments or
; introduce IFs, etc. (see abbreviationp), and we apply those
; unconditional :REWRITE rules with the same property.
; It used to be written:
; Note: In a break with Nqthm and the first four versions of ACL2, in
; Version 1.5 we also expand IMPLIES terms here. In fact, we expand
; several members of *expandable-boot-strap-non-rec-fns* here, and
; IFF. The impetus for this decision was the forcing of impossible
; goals by simplify-clause. As of this writing, we have just added
; the idea of forcing rounds and the concommitant notion that forced
; hypotheses are proved under the type-alist extant at the time of the
; force. But if the simplifer sees IMPLIES terms and rewrites their
; arguments, it does not augment the context, e.g., in (IMPLIES hyps
; concl) concl is rewritten without assuming hyps and thus assumptions
; forced in concl are context free and often impossible to prove. Now
; while the user might hide propositional structure in other functions
; and thus still suffer this failure mode, IMPLIES is the most common
; one and by opening it now we make our context clearer. See the note
; below for the reason we expand other
; *expandable-boot-strap-non-rec-fns*.
; This is no longer true. We now expand the IMPLIES from the original
; theorem in preprocess-clause before expand-abbreviations is called,
; and do not expand any others here. These changes in the handling of
; IMPLIES (as well as several others) are caused by the introduction
; of assume-true-false-if. See the mini-essay at
; assume-true-false-if.
(cond
((zero-depthp rdepth)
(rdepth-error
(mv term ttree)
t))
((time-limit4-reached-p ; nil, or throws
"Out of time in expand-abbreviations.")
(mv nil nil))
((variablep term)
(let ((temp (assoc-eq term alist)))
(cond (temp (mv (cdr temp) ttree))
(t (mv term ttree)))))
((fquotep term) (mv term ttree))
((eq (ffn-symb term) 'hide)
(mv (sublis-var alist term)
ttree))
(t
(mv-let
(expanded-args ttree)
(expand-abbreviations-lst (fargs term)
alist
(geneqv-lst (ffn-symb term) geneqv ens wrld)
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) ens wrld state ttree)
(let* ((fn (ffn-symb term))
(term (cons-term fn expanded-args)))
; If term does not collapse to a constant, fn is still its ffn-symb.
(cond
((fquotep term)
; Term collapsed to a constant. But it wasn't a constant before, and so
; it collapsed because cons-term executed fn on constants. So we record
; a use of the executable counterpart.
(mv term (push-lemma (fn-rune-nume fn nil t wrld) ttree)))
((member-equal fn fns-to-be-ignored-by-rewrite)
(mv (cons-term fn expanded-args) ttree))
((and (all-quoteps expanded-args)
(enabled-xfnp fn ens wrld)
(or (flambda-applicationp term)
(not (getprop fn 'constrainedp nil
'current-acl2-world wrld))))
(cond ((flambda-applicationp term)
(expand-abbreviations
(lambda-body fn)
(pairlis$ (lambda-formals fn) expanded-args)
geneqv
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) ens wrld state ttree))
((programp fn wrld)
; Why is the above test here? We do not allow :program mode fns in theorems.
; However, the prover can be called during definitions, and in particular we
; wind up with the call (SYMBOL-BTREEP NIL) when trying to admit the following
; definition.
#|
(defun symbol-btreep (x)
(if x
(and (true-listp x)
(symbolp (car x))
(symbol-btreep (caddr x))
(symbol-btreep (cdddr x)))
t))
|#
(mv (cons-term fn expanded-args) ttree))
(t
(mv-let
(erp val latches)
(pstk
(ev-fncall fn (strip-cadrs expanded-args)
(f-decrement-big-clock state)
nil
t))
(declare (ignore latches))
(cond
(erp
; We following a suggestion from Matt Wilding and attempt to simplify the term
; before applying HIDE.
(let ((new-term1 (cons-term fn expanded-args)))
(mv-let (new-term2 ttree)
(expand-abbreviations-with-lemma
new-term1 geneqv fns-to-be-ignored-by-rewrite rdepth
ens wrld state ttree)
(cond
((equal new-term2 new-term1)
(mv (mcons-term* 'hide new-term1)
(push-lemma (fn-rune-nume 'hide nil nil wrld)
ttree)))
(t (mv new-term2 ttree))))))
(t (mv (kwote val)
(push-lemma (fn-rune-nume fn nil t wrld)
ttree))))))))
((flambdap fn)
(cond ((abbreviationp nil
(lambda-formals fn)
(lambda-body fn))
(expand-abbreviations
(lambda-body fn)
(pairlis$ (lambda-formals fn) expanded-args)
geneqv
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) ens wrld state ttree))
(t
; Once upon a time (well into v1-9) we just returned (mv term ttree)
; here. But then Jun Sawada pointed out some problems with his proofs
; of some theorems of the form (let (...) (implies (and ...) ...)).
; The problem was that the implies was not getting expanded (because
; the let turns into a lambda and the implication in the body is not
; an abbreviationp, as checked above). So we decided that, in such
; cases, we would actually expand the abbreviations in the body
; without expanding the lambda itself, as we do below. This in turn
; often allows the lambda to expand via the following mechanism.
; Preprocess-clause calls expand-abbreviations and it expands the
; implies into IFs in the body without opening the lambda. But then
; preprocess-clause calls clausify-input which does another
; expand-abbreviations and this time the expansion is allowed. We do
; not imagine that this change will adversely affect proofs, but if
; so, well, the old code is shown on the first line of this comment.
(mv-let (body ttree)
(expand-abbreviations
(lambda-body fn)
nil
geneqv
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) ens wrld state ttree)
; Rockwell Addition:
; Once upon another time (through v2-5) we returned the fcons-term
; shown in the t clause below. But Rockwell proofs indicate that it
; is better to eagerly expand this lambda if the new body would make
; it an abbreviation.
(cond
((abbreviationp nil
(lambda-formals fn)
body)
(expand-abbreviations
body
(pairlis$ (lambda-formals fn) expanded-args)
geneqv
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) ens wrld state ttree))
(t
(mv (mcons-term (list 'lambda (lambda-formals fn)
body)
expanded-args)
ttree)))))))
((member-eq fn '(iff synp prog2$ must-be-equal time$
#+hons memoize-on #+hons memoize-off
with-prover-time-limit force case-split
double-rewrite))
; The list above is an arbitrary subset of *expandable-boot-strap-non-rec-fns*.
; Once upon a time we used the entire list here, but Bishop Brock complained
; that he did not want EQL opened. So we have limited the list to just the
; propositional function IFF and the no-ops.
; Note: Once upon a time we did not expand any propositional functions
; here. Indeed, one might wonder why we do now? The only place
; expand-abbreviations was called was from within preprocess-clause.
; And there, its output was run through clausify-input and then
; remove-trivial-clauses. The latter called tautologyp on each clause
; and that, in turn, expanded all the functions above (but discarded
; the expansion except for purposes of determining tautologyhood).
; Thus, there is no real case to make against expanding these guys.
; For sanity, one might wish to keep the list above in sync with
; that in tautologyp, where we say about it: "The list is in fact
; *expandable-boot-strap-non-rec-fns* with NOT deleted and IFF added.
; The main idea here is to include non-rec functions that users
; typically put into the elegant statements of theorems." But now we
; have deleted IMPLIES from this list, to support the assume-true-false-if
; idea, but we still keep IMPLIES in the list for tautologyp because
; if we can decide it's a tautology by expanding, all the better.
(with-accumulated-persistence
(fn-rune-nume fn nil nil wrld)
(term ttree)
t
(expand-abbreviations (body fn t wrld)
(pairlis$ (formals fn wrld) expanded-args)
geneqv
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) ens wrld state
(push-lemma (fn-rune-nume fn nil nil wrld)
ttree))))
; Rockwell Addition: We are expanding abbreviations. This is new treatment
; of IF, which didn't used to receive any special notice.
((eq fn 'if)
; There are no abbreviation (or rewrite) rules hung on IF, so coming out
; here is ok.
(let ((a (car expanded-args))
(b (cadr expanded-args))
(c (caddr expanded-args)))
(cond
((equal b c) (mv b ttree))
((quotep a)
(mv (if (eq (cadr a) nil) c b) ttree))
((and (equal geneqv *geneqv-iff*)
(equal b *t*)
(or (equal c *nil*)
(and (nvariablep c)
(not (fquotep c))
(eq (ffn-symb c) 'HARD-ERROR))))
; Some users keep HARD-ERROR disabled so that they can figure out
; which guard proof case they are in. HARD-ERROR is identically nil
; and we would really like to eliminate the IF here. So we use our
; knowledge that HARD-ERROR is nil even if it is disabled. We don't
; even put it in the ttree, because for all the user knows this is
; primitive type inference.
(mv a ttree))
(t (mv (mcons-term 'if expanded-args) ttree)))))
; Rockwell Addition: New treatment of equal.
((and (eq fn 'equal)
(equal (car expanded-args) (cadr expanded-args)))
(mv *t* ttree))
(t
(expand-abbreviations-with-lemma
term geneqv fns-to-be-ignored-by-rewrite rdepth ens wrld state
ttree))))))))
(defun expand-and-or
(term bool fns-to-be-ignored-by-rewrite ens wrld state ttree)
; We expand the top-level fn symbol of term provided the expansion
; produces a conjunction -- when bool is nil -- or a disjunction -- when
; bool is t. We return three values: wonp, the new term, and a new ttree.
; This fn is a No-Change Loser.
(cond ((variablep term) (mv nil term ttree))
((fquotep term) (mv nil term ttree))
((member-equal (ffn-symb term) fns-to-be-ignored-by-rewrite)
(mv nil term ttree))
((flambda-applicationp term)
(cond ((and-orp (lambda-body (ffn-symb term)) bool)
(mv-let (term ttree)
(expand-abbreviations
(subcor-var (lambda-formals (ffn-symb term))
(fargs term)
(lambda-body (ffn-symb term)))
nil
*geneqv-iff*
fns-to-be-ignored-by-rewrite
(rewrite-stack-limit wrld) ens wrld state ttree)
(mv t term ttree)))
(t (mv nil term ttree))))
(t
(let ((def-body (def-body (ffn-symb term) wrld)))
(cond
((and def-body
(null (access def-body def-body :recursivep))
(null (access def-body def-body :hyp))
(enabled-numep (access def-body def-body :nume)
ens)
(and-orp (access def-body def-body :concl)
bool))
(mv-let (term ttree)
(with-accumulated-persistence
(access def-body def-body :rune)
(term ttree)
t
(expand-abbreviations
(subcor-var (access def-body def-body
:formals)
(fargs term)
(access def-body def-body :concl))
nil
*geneqv-iff*
fns-to-be-ignored-by-rewrite
(rewrite-stack-limit wrld)
ens wrld state
(push-lemma? (access def-body def-body :rune)
ttree)))
(mv t term ttree)))
(t (mv-let (wonp cr-rune lemma unify-subst)
(find-and-or-lemma
term bool
(getprop (ffn-symb term) 'lemmas nil
'current-acl2-world wrld)
ens wrld)
(cond
(wonp
(mv-let
(term ttree)
(with-accumulated-persistence
(access rewrite-rule lemma :rune)
(term ttree)
t
(expand-abbreviations
(sublis-var unify-subst
(access rewrite-rule lemma :rhs))
nil
*geneqv-iff*
fns-to-be-ignored-by-rewrite
(rewrite-stack-limit wrld)
ens wrld state
(push-lemma cr-rune
(push-lemma (access rewrite-rule lemma
:rune)
ttree))))
(mv t term ttree)))
(t (mv nil term ttree))))))))))
(defun type-set-and-returned-formals-with-rule
(tp term type-alist ens wrld ttree)
; This function is patterned after type-set-with-rule, which the
; reader might understand first.
; The ttree returned is 'assumption-free (provided the initial ttree
; and type-alist are also).
(cond
((enabled-numep (access type-prescription tp :nume) ens)
(mv-let
(unify-ans unify-subst)
(one-way-unify (access type-prescription tp :term)
term)
(cond
(unify-ans
(with-accumulated-persistence
(access type-prescription tp :rune)
(basic-ts vars-ts vars type-alist ttree)
(not (and (ts= basic-ts *ts-unknown*)
(ts= vars-ts *ts-empty*)
(null vars)))
(let ((type-alist (extend-type-alist-with-bindings unify-subst
nil
nil
type-alist
nil
ens wrld
nil
nil nil)))
(mv-let
(relieve-hyps-ans type-alist ttree)
(type-set-relieve-hyps (access type-prescription tp :rune)
term
(access type-prescription tp :hyps)
nil
nil
unify-subst
type-alist
nil ens wrld nil ttree
nil nil)
(cond
(relieve-hyps-ans
; Subject to the conditions in ttree, we now know that the type set of term is
; either in :basic-ts or else that term is equal to the image under unify-subst
; of some var in the :vars of the rule. Our charter is to return five results:
; basic-ts, vars-ts, vars, type-alist and ttree. We do that with the
; subroutine below. It sweeps over the unify-subst, considering each vi and
; its image, ai. If ai is a variable, then it accumulates ai into the returned
; vars (which is initially nil below) and the type-set of ai into vars-ts
; (which is initially *ts-empty* below). If ai is not a variable, it
; accumulates the type-set of ai into basic-ts (which is initially :basic-ts
; below).
(type-set-and-returned-formals-with-rule1
unify-subst
(access type-prescription tp :vars)
type-alist ens wrld
(access type-prescription tp :basic-ts)
*ts-empty*
nil
(push-lemma
(access type-prescription tp :rune)
ttree)))
(t
; We could not establish the hyps of the rule. Thus, the rule tells us
; nothing about term.
(mv *ts-unknown* *ts-empty* nil type-alist ttree)))))))
(t
; The :term of the rule does not unify with our term.
(mv *ts-unknown* *ts-empty* nil type-alist ttree)))))
(t
; The rule is disabled.
(mv *ts-unknown* *ts-empty* nil type-alist ttree))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Final stuff
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(push-untouchable coerce-state-to-object t)
(push-untouchable ev-fncall t)
(progn!
(set-ld-redefinition-action nil state))