; 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))