; 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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; Start up ACL2. Then: ; :q ; (load "patch-3.2-4-raw.lisp") ; (compile-file "patch-3.2-4-raw.lisp") ; Then quit ACL2. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; PATCH USAGE ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; After the above certify-book, you can include this patch by putting the ; following form in your ~/acl2-init.lsp or (GCL only) ./init.lsp file. ; (load (concatenate 'string "patch-3.2-4-raw." acl2::*compiled-file-extension*)) ; You will probably want to add an absolute pathname, e.g.: ; (load (concatenate 'string "/u/smith/acl2/" "patch-3.2-4-raw." acl2::*compiled-file-extension*)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; 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)) 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. ||# ; Please use the certifiable book patch-3.2-4.lisp instead if you want the ; following additional patches. #|| 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. Added coverage of :meta rules to the accumulated-persistence statistics. ||# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; CODE ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; Fix for soundness bug related to mbe and mv ;;; and for bug in evaluation of calls of with-prover-time-limit ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (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)))))))))))))))))))