diff options
Diffstat (limited to 'books/workshops/2007/erickson/bprove')
| -rw-r--r-- | books/workshops/2007/erickson/bprove/Readme.lsp | 36 | ||||
| -rw-r--r-- | books/workshops/2007/erickson/bprove/bash.lisp | 287 | ||||
| -rw-r--r-- | books/workshops/2007/erickson/bprove/exdefs.lisp | 41 | ||||
| -rw-r--r-- | books/workshops/2007/erickson/bprove/gen.lisp | 337 | ||||
| -rw-r--r-- | books/workshops/2007/erickson/bprove/lemgen.lisp | 1373 | ||||
| -rw-r--r-- | books/workshops/2007/erickson/bprove/refute.lisp | 302 |
6 files changed, 2376 insertions, 0 deletions
diff --git a/books/workshops/2007/erickson/bprove/Readme.lsp b/books/workshops/2007/erickson/bprove/Readme.lsp new file mode 100644 index 0000000..28c6b4e --- /dev/null +++ b/books/workshops/2007/erickson/bprove/Readme.lsp @@ -0,0 +1,36 @@ +; A simple example of a book directory +; Copyright (C) 2006 University of Texas at Austin + +((:FILES ; non-empty list of filenames, generated from Unix command "ls -1R" + " +.: +Makefile +Readme.lsp +bash.lisp +exdefs.lisp +gen.lisp +lemgen.lisp +refute.lisp +") + (:TITLE "Backtracking Prover") + (:AUTHOR/S "J. Erickson") ; non-empty list of author strings + (:KEYWORDS ; non-empty list of keywords, case-insensitive + "book contributions" "contributed books" "induction" "generalization" "backtracking") + (:ABSTRACT "Book for paper ``Backtracking and Induction in ACL2'', ACL2 Workshop 2007") + (:PERMISSION ; author/s permission for distribution and copying: + "Copyright (C) 2007 John Erickson + +This program is free software; you can redistribute it and/or modify +it under the terms of Version 2 of the GNU General Public License as +published by the Free Software Foundation. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software +Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA +02110-1301, USA.")) + diff --git a/books/workshops/2007/erickson/bprove/bash.lisp b/books/workshops/2007/erickson/bprove/bash.lisp new file mode 100644 index 0000000..915d667 --- /dev/null +++ b/books/workshops/2007/erickson/bprove/bash.lisp @@ -0,0 +1,287 @@ +; Copyright (C) 2006 University of Texas at Austin + +; This program is free software; you can redistribute it and/or modify it under +; the terms of Version 2 of the GNU General Public License as published by the +; Free Software Foundation. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Matt Kaufmann +; email: Kaufmann@cs.utexas.edu +; Department of Computer Science +; University of Texas at Austin +; Austin, TX 78701 U.S.A. + +; October, 2006 + +; [Note added by Matt Kaufmann on May 5, 2012: I believe that this book, in +; John Erickson's books/workshops/2007/erickson/bprove/, was based on a version +; of my books/misc/bash.lisp book. I see a modification to +; simplify-with-prover that comments out fertilize and eliminate-destructors. +; I don't know if anything else was modified, but for now I'll just keep this +; book as it currently stands rather than trying to bring it up to date with +; books/misc/bash.lisp.] + +; In a nutshell: + +; If you submit (bash term), then the result is a list of goals to which ACL2 +; can simplify term when attempting to prove it. (In particular, if the result +; is nil, then ACL2 can prove term.) More accurately: (bash term) returns (mv +; erp val state), where: erp is nil unless there is an error; and val is a list +; of terms, in untranslated (user-level) form, whose provability implies the +; provability of the input term. If ACL2 cannot simplify the input term, then +; there is an error, i.e., erp is not nil. + +; More details: + +; This book defines a utility similar to the proof-builder's bash command, but +; for use in the top-level loop. The input term can be a user-level term, +; i.e., it need not be translated. Thus this bash utility is given a term, and +; it returns an error triple (mv erp termlist state) where if erp is not nil, +; then termlist is the list of goals that ACL2 would get stuck on, if you were +; to attempt to prove the given term with only simplification, i.e., with a +; "Goal" hint of :do-not '(generalize eliminate-destructors fertilize +; eliminate-irrelevance) and with induction turned off. Bash does all the +; normal simplification stuff, including forward chaining. Use :hints to +; specify hints using the same syntax as for thm and defthm. Use a non-nil +; value of :verbose if you want output, including the proof attempt. The +; keyword values are not evaluated, so :hints could be of the form (("Goal +; ...)) but not '(("Goal" ...)). + +; This book also includes a functional (non-macro) version of bash, bash-fn. +; At the end is a variant contributed by Dave Greve, bash-term-to-dnf, that +; returns a list of goals (implicitly conjoined) where each goal has the form +; (lit1 lit2 ... litk), for which the goal is equivalent to the negation of the +; conjunction of the liti. + +; Examples: + +#| +ACL2 !>(bash (equal (append x y) (append (car (cons x a)) z))) + ((EQUAL (APPEND X Y) (APPEND X Z))) +ACL2 !>(bash (equal (car (cons x y)) x)) + NIL +ACL2 !>(bash (implies (true-listp x) (equal (append x y) zzz)) + :hints (("Goal" :expand ((true-listp x) + (true-listp (cdr x)) + (append x y))))) + ((EQUAL Y ZZZ) + (IMPLIES (AND (CONSP X) + (CONSP (CDR X)) + (TRUE-LISTP (CDDR X))) + (EQUAL (LIST* (CAR X) + (CADR X) + (APPEND (CDDR X) Y)) + ZZZ)) + (IMPLIES (AND (CONSP X) (NOT (CDR X))) + (EQUAL (CONS (CAR X) Y) ZZZ))) +ACL2 !>(bash-term-to-dnf + '(implies (true-listp x) (equal (append x y) zzz)) + '(("Goal" :expand ((true-listp x) + (true-listp (cdr x)) + (append x y)))) + nil state) + (((EQUAL Y ZZZ)) + ((NOT (CONSP X)) + (NOT (CONSP (CDR X))) + (NOT (TRUE-LISTP (CDDR X))) + (EQUAL (LIST* (CAR X) + (CADR X) + (APPEND (CDDR X) Y)) + ZZZ)) + ((NOT (CONSP X)) + (CDR X) + (EQUAL (CONS (CAR X) Y) ZZZ))) +ACL2 !> +|# ; | + +(in-package "ACL2") + +(program) + +(set-state-ok t) + +; The following appears in the ACL2 source code, but is included temporarily +; for a few days pending some users updating to a sufficiently recent +; development snapshot. +(defun unproved-pc-prove-clauses (ttree) + (reverse-strip-cdrs (tagged-objects :bye ttree) nil)) + +(defun simplify-with-prover (form hints ctx state) + +; This is patterned after (define-pc-primitive prove ...). + + (let ((wrld (w state)) + (ens (ens state)) + (name-tree 'bash)) + (er-let* + ((thints (translate-hints + name-tree + +; Keep the following in sync with the definition of the proof-builder :bash +; command. + + (append + *bash-skip-forcing-round-hints* + (add-string-val-pair-to-string-val-alist + "Goal" + :do-not + (list 'quote '(generalize ;eliminate-destructors + ;fertilize + eliminate-irrelevance)) + (add-string-val-pair-to-string-val-alist + "Goal" + :do-not-induct + name-tree + hints)) + (default-hints wrld)) + ctx wrld state)) + (tterm (translate form t t t ctx wrld state))) + (mv-let (erp ttree state) + (pc-prove tterm form thints t ens wrld ctx state) + (cond (erp (mv t nil state)) + (t (let ((clauses (unproved-pc-prove-clauses ttree))) + (cond ((and (eql (length clauses) 1) + (eql (length (car clauses)) 1) + (eql (caar clauses) tterm)) + (mv 'no-change nil state)) + (t (value clauses)))))))))) + +(defun simplify-with-prover2 (form hints ctx state) + +; This is patterned after (define-pc-primitive prove ...). + + (let ((wrld (w state)) + (ens (ens state)) + (name-tree 'bash)) + (er-let* + ((thints (translate-hints + name-tree + +; Keep the following in sync with the definition of the proof-builder :bash +; command. + + (append + *bash-skip-forcing-round-hints* + (add-string-val-pair-to-string-val-alist + "Goal" + :do-not + (list 'quote '(generalize eliminate-destructors + ;fertilize + eliminate-irrelevance)) + (add-string-val-pair-to-string-val-alist + "Goal" + :do-not-induct + name-tree + hints)) + (default-hints wrld)) + ctx wrld state)) + (tterm (translate form t t t ctx wrld state))) + (mv-let (erp ttree state) + (pc-prove tterm form thints t ens wrld ctx state) + (cond (erp (mv t nil state)) + (t (let ((clauses (unproved-pc-prove-clauses ttree))) + (cond ((and (eql (length clauses) 1) + (eql (length (car clauses)) 1) + (eql (caar clauses) tterm)) + (mv 'no-change nil state)) + (t (value clauses)))))))))) + +(defun bash-fn (form hints verbose ctx state) + +; Keep this in sync with bash-term-to-dnf. + + (mv-let + (erp clauses state) + (cond (verbose + (simplify-with-prover form hints ctx state)) + (t + (state-global-let* + ((inhibit-output-lst *valid-output-names*)) + (simplify-with-prover form hints ctx state)))) + (cond + (erp + (pprogn + (warning$ ctx "bash" + "Unable to simplify the input term~@0" + (cond ((eq erp 'no-change) + ".") + (t (msg " because an error occurred.~@0" + (cond + (verbose "") + (t " Try setting the verbose flag to t in ~ + order to see what is going on.")))))) + (value (list form)))) + (t + (value (prettyify-clause-lst clauses (let*-abstractionp state) (w state))))))) + +(defmacro bash (term &key verbose hints) + `(bash-fn ',term ',hints ',verbose 'bash state)) + +; Dave Greve has contributed the following (only slightly modified here), to +; create a variant bash-term-to-dnf of bash-fn. This example may suggest other +; variants; feel free to contribute yours to Matt Kaufmann, +; kaufmann@cs.utexas.edu. + +(defun goals-to-cnf (goals) + (cond ((endp goals) nil) + (t (cons (append (access goal (car goals) :hyps) + (list (dumb-negate-lit (access goal (car goals) + :conc)))) + (goals-to-cnf (cdr goals)))))) + +(defun untranslate-lst-lst (list iff-flg wrld) + (cond + ((endp list) + nil) + (t (cons (untranslate-lst (car list) iff-flg wrld) + (untranslate-lst-lst (cdr list) iff-flg wrld))))) + +(defun bash-term-to-dnf (form hints verbose state) + +; Keep this in sync with bash-fn. + + (let ((ctx 'bash-term-to-dnf)) + (mv-let + (erp clauses state) + (cond (verbose + (simplify-with-prover form hints ctx state)) + (t + (state-global-let* + ((inhibit-output-lst *valid-output-names*)) + (simplify-with-prover form hints ctx state)))) + (cond + (erp + (pprogn + (value (list (list form))))) + (t + (value clauses)))))) + + +;no dtor or fertilize +(defun bash-term-to-dnf2 (form hints verbose state) + +; Keep this in sync with bash-fn. + + (let ((ctx 'bash-term-to-dnf)) + (mv-let + (erp clauses state) + (cond (verbose + (simplify-with-prover2 form hints ctx state)) + (t + (state-global-let* + ((inhibit-output-lst *valid-output-names*)) + (simplify-with-prover2 form hints ctx state)))) + (cond + (erp + (pprogn + (value (list (list form))))) + (t + (value clauses)))))) diff --git a/books/workshops/2007/erickson/bprove/exdefs.lisp b/books/workshops/2007/erickson/bprove/exdefs.lisp new file mode 100644 index 0000000..c831cea --- /dev/null +++ b/books/workshops/2007/erickson/bprove/exdefs.lisp @@ -0,0 +1,41 @@ +(in-package "ACL2") + +(include-book "lemgen") + + +(defun ilen (x a) + (if (endp x) + a + (ilen (cdr x) (1+ a)))) + +(defun rot2 (i x) + (if (endp i) + x + (rot2 (cdr i) (append (cdr x) (list (car x)))))) + +(defun rv1 (x a) + (if (endp x) + a + (rv1 (cdr x) (cons (car x) a)))) + + +(make-event + +; Added by Matt K. after v5-0. Apparently bprove doesn't call +; initialize-summary-accumulators, which is what invokes (time-tracker :tau +; :init ...). So we take the easy way out here and turn off time-tracker +; during certification. If someone decides to use bprove outside this +; directory, that person can figure out how to initialize the time-tracker for +; tag :tau as it's done in initialize-summary-accumulators. + + (prog2$ (time-tracker nil) + (value '(value-triple nil)))) + +(bprove (equal (rv1 x 'nil) (rv x))) + +(bprove (equal (ilen x '0) (len x))) + +(bprove (implies (and (true-listp x)) (equal (rot2 x x) x))) + +(bprove (implies (and (true-listp x) (true-listp y)) (equal (rot2 x (append x y)) (append y x)))) + diff --git a/books/workshops/2007/erickson/bprove/gen.lisp b/books/workshops/2007/erickson/bprove/gen.lisp new file mode 100644 index 0000000..307f555 --- /dev/null +++ b/books/workshops/2007/erickson/bprove/gen.lisp @@ -0,0 +1,337 @@ +(in-package "ACL2") + +(set-ignore-ok t) + +(set-irrelevant-formals-ok t) + +(set-state-ok t) + +(program) + +; And now we do generalization... + +(defun collectable-fnp2 (fn ens wrld) + +; A common collectable term is a non-quoted term that is an +; application of a collectable-fnp2. Most functions are common +; collectable. The ones that are not are cons, open lambdas, and the +; (enabled) destructors of wrld. + + t) + +(mutual-recursion + +(defun smallest-common-subterms12 (term1 term2 ens wrld ans) + +; This is the workhorse of smallest-common-subterms, but the arguments are +; arranged so that we know that term1 is the smaller. We add to ans +; every subterm x of term1 that (a) occurs in term2, (b) is +; collectable, and (c) has no collectable subterms in common with +; term2. + +; We return two values. The first is the modified ans. The second is +; t or nil according to whether term1 occurs in term2 but neither it +; nor any of its subterms is collectable. This latter condition is +; said to be the ``potential'' of term1 participating in a collection +; vicariously. What does that mean? Suppose a1, ..., an, all have +; potential. Then none of them are collected (because they aren't +; collectable) but each occurs in term2. Thus, a term such as (fn a1 +; ... an) might actually be collected because it may occur in term2 +; (all of its args do, at least), it may be collectable, and none of +; its subterms are. So those ai have the potential to participate +; vicariously in a collection. + + (cond ((or (variablep term1) + ) + +; Since term1 is not collectable, we don't add it to ans. But we return +; t as our second value if term1 occurs in term2, i.e., term1 has +; potential. + + (mv ans (occur term1 term2))) + ((fquotep term1) + (if (occur term1 term2) + (mv (add-to-set-equal term1 ans) + nil) + (mv ans nil))) + + (t + (if (occur term1 term2) + (mv (add-to-set-equal term1 ans) + nil) + (mv-let + (ans all-potentials) + (smallest-common-subterms12-lst (fargs term1) term2 ens wrld ans) + (cond ((null all-potentials) + +; Ok, some arg did not have potential. Either it did not occur or it +; was collected. In either case, term1 should not be collected and +; furthermore, has no potential for participating later. + + (mv ans nil)) + ((not (occur term1 term2)) + +; Every arg of term1 had potential but term1 doesn't occur in +; term2. That means we don't collect it and it hasn't got +; potential. + (mv ans nil)) + ((collectable-fnp2 (ffn-symb term1) ens wrld) + +; So term1 occurs, none of its subterms were collected, and term1 +; is collectable. So we collect it, but it no longer has potential +; (because it got collected). + + (mv (add-to-set-equal term1 ans) + nil)) + + (t + +; Term1 occurs, none of its subterms were collected, and term1 +; was not collected. So it has potential to participate vicariously. + + (mv ans t)))))))) + +(defun smallest-common-subterms12-lst (terms term2 ens wrld ans) + +; We accumulate onto ans every subterm of every element of terms +; that (a) occurs in term2, (b) is collectable, and (c) has no +; collectable subterms in common with term2. We return the modified +; ans and the flag indicating whether all of the terms have potential. + + (cond + ((null terms) (mv ans t)) + (t (mv-let + (ans car-potential) + (smallest-common-subterms12 (car terms) term2 ens wrld ans) + (mv-let + (ans cdr-potential) + (smallest-common-subterms12-lst (cdr terms) term2 ens wrld ans) + (mv ans + (and car-potential + cdr-potential))))))) + +) + +(defun dumb-fn-count-1 (flg x acc) + (declare (xargs :guard (and (if flg + (pseudo-term-listp x) + (pseudo-termp x)) + (natp acc)))) + (cond (flg (cond ((null x) + acc) + (t + (dumb-fn-count-1 t (cdr x) + (dumb-fn-count-1 nil (car x) acc))))) + ((or (variablep x) (fquotep x)) + acc) + (t (dumb-fn-count-1 t (fargs x) (1+ acc))))) + +(defun dumb-fn-count (x) + +; Originally we had this upside-down call tree, where cons-count was a function +; that counts the number of conses in an object. + +; cons-count +; smallest-common-subterms +; generalizable-terms-across-relations +; generalizable-terms +; generalizable-terms-across-literals1 +; generalizable-terms-across-literals +; generalizable-terms +; generalize-clause + +; But the role of evgs disappears if we use dumb-occur instead of occur in our +; algorithm for finding common subterms, which seems anyhow like the right +; thing to do if the point is to generalize common subterms to variables. +; Evg-occur is called by occur but not by dumb-occur, and evg-occur is +; potentially expensive on galactic objects. So we no longer use cons-count to +; compute the smallest-common-subterms; we use fn-count-dumb. + + (dumb-fn-count-1 nil x 0)) + +(defun smallest-common-subterms2 (term1 term2 ens wrld ans) + +; We accumulate onto ans and return the list of every subterm x of +; term1 that is also a subterm of term2, provided x is ``collectable'' +; and no subterm of x is collectable. A term is a collectable if it +; is an application of a collectable-fnp2 and is not an explicit value. +; Our aim is to collect the ``innermost'' or ``smallest'' collectable +; subterms. + + (mv-let (ans potential) + (cond ((> (dumb-fn-count term1) (dumb-fn-count term2)) + (smallest-common-subterms12 term2 term1 ens wrld ans)) + (t (smallest-common-subterms12 term1 term2 ens wrld ans))) + (declare (ignore potential)) + ans)) + +(defun generalizing-relationp2 (term wrld) + +; Term occurs as a literal of a clause. We want to know whether +; we should generalize common subterms occurring in its arguments. +; Right now the answer is geared to the special case that term is +; a binary relation -- or at least that only two of the arguments +; encourage generalizations. We return three results. The first +; is t or nil indicating whether the other two are important. +; The other two are the two terms we should explore for common +; subterms. + +; For example, for (equal lhs rhs), (not (equal lhs rhs)), (< lhs +; rhs), and (not (< lhs rhs)), we return t, lhs, and rhs. We also +; generalize across any known equivalence relation, but this code has +; built into the assumption that all such relations have arity at +; least 2 and just returns the first two args. For (member x y), we +; return three nils. + + (mv-let (neg-flg atm) + (strip-not term) + (declare (ignore neg-flg)) + (cond ((or (variablep atm) + (fquotep atm) + (flambda-applicationp atm)) + (mv nil nil nil)) + ((or (eq (ffn-symb atm) 'equal) + (eq (ffn-symb atm) '<) + (equivalence-relationp (ffn-symb atm) wrld)) + (mv t (fargn atm 1) (fargn atm 2))) + (t (mv nil nil nil))))) + +(defun generalizable-terms-across-relations2 (cl ens wrld ans) + +; We scan clause cl for each literal that is a generalizing-relationp2, +; e.g., (equal lhs rhs), and collect into ans all the smallest common +; subterms that occur in each lhs and rhs. We return the final ans. + + (cond ((null cl) ans) + (t (mv-let (genp lhs rhs) + (generalizing-relationp2 (car cl) wrld) + (generalizable-terms-across-relations2 + (cdr cl) ens wrld + (if genp + (smallest-common-subterms2 lhs rhs ens wrld ans) + ans)))))) + +(defun generalizable-terms-across-literals12 (lit1 cl ens wrld ans) + (cond ((null cl) ans) + (t (generalizable-terms-across-literals12 + lit1 (cdr cl) ens wrld + (smallest-common-subterms2 lit1 (car cl) ens wrld ans))))) + +(defun generalizable-terms-across-literals2 (cl ens wrld ans) + +; We consider each pair of literals, lit1 and lit2, in cl and +; collect into ans the smallest common subterms that occur in +; both lit1 and lit2. We return the final ans. + + (cond ((null cl) ans) + (t (generalizable-terms-across-literals2 + (cdr cl) ens wrld + (generalizable-terms-across-literals12 (car cl) (cdr cl) + ens wrld ans))))) + +(defun generalizable-terms2 (cl ens wrld) + +; We return the list of all the subterms of cl that we will generalize. +; We look for common subterms across equalities and inequalities, and +; for common subterms between the literals of cl. + + (generalizable-terms-across-literals2 + cl ens wrld + (generalizable-terms-across-relations2 + cl ens wrld nil))) + +(mutual-recursion + (defun quote-types (x) + (if (atom x) + nil + (if (and (quotep x) + (acl2-numberp (cadr x))) + `((not (acl2-numberp ,x))) + (quote-types-l (cdr x))))) + (defun quote-types-l (x) + (if (endp x) + nil + (append (quote-types (car x)) + (quote-types-l (cdr x)))))) + +(defun generalize-clause2 (cl hist pspv wrld state) + +; A standard clause processor of the waterfall. + +; We return 4 values. The first is a signal that is either 'hit, or +; 'miss. When the signal is 'miss, the other 3 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 generalization, and the fourth is an +; unmodified pspv. (We return the fourth thing to adhere to the +; convention used by all clause processors in the waterfall (q.v.).) +; The ttree we return is 'assumption-free. + + (declare (ignore state)) + (cond + ((not (assoc-eq 'being-proved-by-induction + (access prove-spec-var pspv :pool))) + (mv 'miss nil nil nil)) + (t (let* ((ens (access rewrite-constant + (access prove-spec-var + pspv + :rewrite-constant) + :current-enabled-structure)) + (terms (generalizable-terms2 cl ens wrld))) + (cond + ((null terms) + (mv 'miss nil nil nil)) + (t + (let ((cl (append (quote-types-l cl) cl))) + (mv-let + (contradictionp type-alist ttree) + (type-alist-clause cl nil t nil ens wrld + nil nil) + (declare (ignore ttree)) + (cond + (contradictionp + +; We compute the type-alist of the clause to allow us to generate nice +; variable names and to restrict the coming generalization. We know +; that a contradiction cannot arise, because this clause survived +; simplification. However, we will return an accurate answer just to +; be rugged. We'll report that we couldn't do anything! That's +; really funny. We just proved our goal and we're saying we can't do +; anything. But if we made this fn sometimes return the empty set of +; clauses we'd want to fix the io handler for it and we'd have to +; respect the 'assumptions in the ttree and we don't. Do we? As +; usual, we ignore the ttree in this case, and hence we ignore it +; totally since it is known to be nil when contradictionp is nil. + + (mv 'miss nil nil nil)) + (t + (let ((gen-vars + (generate-variable-lst terms + (all-vars1-lst cl + (owned-vars + 'generalize-clause2 + nil + hist)) + type-alist ens wrld))) + (mv-let (generalized-cl restricted-vars var-to-runes-alist ttree) + (generalize1 cl type-alist terms gen-vars ens wrld) + (mv 'hit + (list generalized-cl) + (add-to-tag-tree + 'variables gen-vars + (add-to-tag-tree + 'terms terms + (add-to-tag-tree + 'restricted-vars restricted-vars + (add-to-tag-tree + 'var-to-runes-alist var-to-runes-alist + (add-to-tag-tree + 'ts-ttree ttree + nil))))) + pspv))))))))))))) + + +;(defun unhidden-lit-info (hist clause pos wrld) (mv nil nil nil)) + +;(defun cross-fertilizep/c (equiv cl direction lhs1 rhs1) t) + diff --git a/books/workshops/2007/erickson/bprove/lemgen.lisp b/books/workshops/2007/erickson/bprove/lemgen.lisp new file mode 100644 index 0000000..9d99b9a --- /dev/null +++ b/books/workshops/2007/erickson/bprove/lemgen.lisp @@ -0,0 +1,1373 @@ +(in-package "ACL2") + +(include-book "refute") +;(include-book "exdefs") +(include-book "gen") + +;(include-book "bash3") +;(include-book "../induct/myutil") +;(include-book "cprove") + +(set-state-ok t) + +;(set-ld-redefinition-action '(:doit . :overwrite) state) + +(set-ignore-ok t) +(set-irrelevant-formals-ok t) + + +(logic) + +(defthm car-ap-cons + (equal (car (append (cons a b) c)) + a)) + +(defthm cdr-ap-cons + (equal (cdr (append (cons a nil) c)) + c)) + +(defthm append-cons (CONSP (BINARY-APPEND (CONS X3 'NIL) z)) :rule-classes :type-prescription) + +(defthm cons-ap + (implies (syntaxp (not (equal x ''nil))) + (equal (cons a x) + (append (cons a nil) x)))) + +;(defthm cons-ap-ap +; (implies (syntaxp (not (equal x ''nil))) +; (equal (append (append (cons a x) y) z) +; (append (cons a nil) (append x y))))) + + +(defthm ap-ap + (equal (append (append x y) z) (append x y z))) + +(program) + + + +(defun basicp (x) + (if (endp x) + t + (and + (atom (car x)) + (basicp (cdr x))))) + +(defun basic-on-call (x c) + (if (endp x) + t + (and (or (atom (car c)) + (atom (car x))) + (basic-on-call (cdr x) (cdr c))))) + +(defun basic-on-calls (x l) + (if (endp l) + t + (and (basic-on-call (cdr x) (cdr (car l))) + (basic-on-calls x (cdr l))))) + +(defun get-calls (l) + (if (endp l) + nil + (append (cddr (car l)) + (get-calls (cdr l))))) + +(defun ind-vars-basicp (x state) + (let* ((im (getprop (car x) 'induction-machine nil 'current-acl2-world (w state))) + (calls (get-calls im))) + (if (null im) + nil + (basic-on-calls x calls)))) + +;(ind-vars-basicp '(BINARY-APPEND Y (CONS X1 'NIL)) state) + +(mutual-recursion + (defun get-schemes (x state) + (if (atom x) + nil + (append + (if (ind-vars-basicp x state) + (list x) + nil) + (get-schemes-l (cdr x) state)))) + (defun get-schemes-l (x state) + (if (endp x) + nil + (append (get-schemes (car x) state) + (get-schemes-l (cdr x) state))))) + + +;(get-schemes '(implies (equal (rv (rv x)) x))) + +;(get-schemes '(implies (and (true-listp x) (true-listp y)) (equal (rot2 x (ap x y)) (ap y x)))) + +;(TRANSLATE '(implies (and (true-listp x) (true-listp y)) (equal (rot2 x (append x y)) (append y x))) nil NIL nil nil (W state) STATE) + + +(mutual-recursion + (defun expand-implies (x) + (if (atom x) + x + (let ((cdrx (expand-implies-l (cdr x)))) + (if (eq (car x) 'implies) + (mv-let (b err) (pmatch-l '(p q) cdrx nil) (declare (ignore err)) + (inst '(IF P (IF Q T NIL) T) b)) + (cons (car x) cdrx))))) + (defun expand-implies-l (x) + (if (endp x) + nil + (cons (expand-implies (car x)) + (expand-implies-l (cdr x)))))) + +#| +(expand-implies + '(IMPLIES (IF (TRUE-LISTP X) (TRUE-LISTP Y) 'NIL) + (EQUAL (ROT2 X (BINARY-APPEND X Y)) + (BINARY-APPEND Y X)))) +|# + + +#| +(clausify '(IF (IF (TRUE-LISTP X) (TRUE-LISTP Y) 'NIL) + (IF (EQUAL (ROT2 X (BINARY-APPEND X Y)) + (BINARY-APPEND Y X)) + T NIL) + T) nil nil (sr-limit (w state))) +|# + +(defun triv-clause (x) + (if (endp x) + nil + (if (eq (car x) t) + t + (triv-clause (cdr x))))) + +(defun simp-clause (x) + (if (endp x) + nil + (if (eq (car x) nil) + (simp-clause (cdr x)) + (cons (car x) (simp-clause (cdr x)))))) + +(defun simp-and-filter (x) + (if (endp x) + nil + (if (triv-clause (car x)) + (simp-and-filter (cdr x)) + (cons (simp-clause (car x)) + (simp-and-filter (cdr x)))))) + +(set-state-ok t) +(set-ignore-ok t) + + +(defun norm (x state) + (mv-let (nop x state) (TRANSLATE x nil NIL nil nil (W state) STATE) + (let* ((x (expand-implies x)) + (x (clausify x nil nil (sr-limit (w state)))) + (x (simp-and-filter x))) + (mv x state)))) + +(defun norm-l (x state) + (if (endp x) + (mv nil state) + (mv-let (r state) (norm (car x) state) + (mv-let (r2 state) (norm-l (cdr x) state) + (mv (append r r2) state))))) + + +;(norm '(implies (and (true-listp x) (true-listp y)) (equal (rot2 x (append x y)) (append y x))) state) + +#| +(get-schemes-l '((NOT (TRUE-LISTP X)) + (NOT (TRUE-LISTP Y)) + (EQUAL (ROT2 X (BINARY-APPEND X Y)) + (BINARY-APPEND Y X)))) + + + +|# + + +(defun new-fsymbol (n) + (intern (concatenate 'string "G" (coerce (explode-nonnegative-integer n 10 nil) 'string)) "ACL2")) + +(defun new-var (n) + (intern (concatenate 'string "NV" (coerce (explode-nonnegative-integer n 10 nil) 'string)) "ACL2")) + +(defun new-thm (n) + (intern (concatenate 'string "T" (coerce (explode-nonnegative-integer n 10 nil) 'string)) "ACL2")) + +(defun new-ifn (n) + (intern (concatenate 'string "IFN" (coerce (explode-nonnegative-integer n 10 nil) 'string)) "ACL2")) + +(defun new-label (n) + (intern (concatenate 'string "L" (coerce (explode-nonnegative-integer n 10 nil) 'string)) "ACL2")) + + + +(program) + + +(defun err-fun () t) +;(trace! (err-fun :entry (break))) + + +(defrec pv (bind schemes log max-fun max-var max-ifn max-thm max-label depth) t) + + +(mutual-recursion +(defun intro-constr-funs (x ind-vars all-vars bind pv state) + (if (atom x) + (if (member x ind-vars) + (mv x bind pv state) + (if (assoc x bind) + (mv (cadr (assoc x bind)) bind pv state) + (let* ((nf (new-fsymbol (access pv pv :max-fun))) + (nc `(,nf ,@all-vars)) + (pv (change pv pv :max-fun (1+ (access pv pv :max-fun)))) + (bind (cons (list x nc) bind))) + (mv-let (erp val state) (ld (list `(defstub ,nf (,@all-vars) t))) + (if (or erp (equal val :error)) + (mv (err-fun) bind pv state) + (let ((pv (change pv pv :log (append + (access pv pv :log) + (list `(defstub ,nf (,@all-vars) t)))))) + (mv nc bind pv state))))))) + (if (quotep x) + (mv x bind pv state) + (mv-let (r bind pv state) (intro-constr-funs-l (cdr x) ind-vars all-vars bind pv state) + (mv (cons (car x) r) bind pv state))))) +(defun intro-constr-funs-l (x ind-vars all-vars bind pv state) + (if (endp x) + (mv nil bind pv state) + (mv-let (r bind pv state) (intro-constr-funs (car x) ind-vars all-vars bind pv state) + (mv-let (r2 bind pv state) (intro-constr-funs-l (cdr x) ind-vars all-vars bind pv state) + (mv (cons r r2) bind pv state)))))) + + + +(defun rm-nop-subs (x) + (if (endp x) + nil + (if (equal (car (car x)) (cadr (car x))) + (rm-nop-subs (cdr x)) + (cons (car x) (rm-nop-subs (cdr x)))))) + +(defun strip-unmeas (x m) + (if (endp x) + nil + (if (member-equal (car (car x)) m) + (cons (car x) (strip-unmeas (cdr x) m)) + (strip-unmeas (cdr x) m)))) + +(defun ih-from-calls (x varsub fcall calls measured pv state) + (if (endp calls) + (mv nil nil pv state) + (let* ((call (car calls))) + (mv-let (isub err) (pmatch fcall call nil) + (let ((isub (strip-unmeas isub measured))) + (let ((realsub (inst-ll isub varsub))) + (mv-let (r bind pv state) + (intro-constr-funs + (inst x realsub) + (strip-cars realsub) + (all-vars x) + nil + pv + state) + (mv-let (r2 calls2 pv state) + (ih-from-calls x varsub + fcall + (cdr calls) + measured + pv + state) + (mv (cons r r2) (append (list (append realsub bind)) calls2) pv state))))))))) + + + + +(defun subgoal-from-tc (x scheme tests calls just pv state) + (let* ((fmls (formals (car scheme) (w state))) + (fcall `(,(car scheme) ,@fmls)) + (measured (cadr just))) + (mv-let (varsub err) (pmatch fcall scheme nil) ; a variable may match twice? + (mv-let (r subs pv state) + (ih-from-calls x varsub fcall calls measured pv state) + (mv `(implies + (and + ,@(inst-l tests varsub) + ,@r) + ,x) + (list (inst-l tests varsub) subs) pv state))))) + + +(defun subgoals-from-im (x scheme im just pv state) + (if (endp im) + (mv nil nil pv state) + (let ((tests (cadr (car im))) + (calls (cddr (car im)))) + (mv-let (r tc pv state) (subgoal-from-tc x scheme tests calls just pv state) + (mv-let (r2 tcl pv state) (subgoals-from-im x scheme (cdr im) just pv state) + (mv (cons r r2) (cons tc tcl) pv state)))))) + +(defun get-induct-goals (x scheme pv state) + (let ((im (getprop (car scheme) 'induction-machine nil 'current-acl2-world (w state))) + (just (getprop (car scheme) 'justification nil 'current-acl2-world (w state)))) + (mv-let (r tcs pv state) (subgoals-from-im x scheme im just pv state) + (mv t r tcs pv state)))) + +(logic) +(defstub goo (x y) t) + +(defun foo (x) + (if (atom x) + nil + (cons (foo (car x)) (foo (cdr x))))) +(program) + + ;(get-induct-goals '(goo x y) '(foo x) state) + + ;(get-induct-goals '(implies (and (true-listp x) (true-listp y)) (equal (rot2 x (append x y)) (append y x))) '(true-listp x) 0 state) + + #| + +(wfall '(IMPLIES (AND (CONSP X) + (IMPLIES (AND (TRUE-LISTP (CDR X)) + (TRUE-LISTP (G0 Y X))) + (EQUAL (ROT2 (CDR X) (APPEND (CDR X) (G0 Y X))) + (APPEND (G0 Y X) (CDR X))))) + (IMPLIES (AND (TRUE-LISTP X) (TRUE-LISTP Y)) + (EQUAL (ROT2 X (APPEND X Y)) + (APPEND Y X)))) state) + +(wfall '(IMPLIES (AND (NOT (CONSP X))) + (IMPLIES (AND (TRUE-LISTP X) (TRUE-LISTP Y)) + (EQUAL (ROT2 X (APPEND X Y)) + (APPEND Y X)))) state) + +(wfall '(and (IMPLIES (AND (CONSP X) + (IMPLIES (AND (TRUE-LISTP (CDR X)) + (TRUE-LISTP (G0 Y X))) + (EQUAL (ROT2 (CDR X) (APPEND (CDR X) (G0 Y X))) + (APPEND (G0 Y X) (CDR X))))) + (IMPLIES (AND (TRUE-LISTP X) (TRUE-LISTP Y)) + (EQUAL (ROT2 X (APPEND X Y)) + (APPEND Y X)))) + (IMPLIES (AND (NOT (CONSP X))) + (IMPLIES (AND (TRUE-LISTP X) (TRUE-LISTP Y)) + (EQUAL (ROT2 X (APPEND X Y)) + (APPEND Y X))))) state) + + +|# + + +(mutual-recursion + (defun find-rec2 (x p state) + (if (atom x) + (mv nil state) + (mv-let (r state) (find-rec2-l (cdr x) p 1 state) + (if (recp x state) + (mv (cons p r) state) + (mv r state))))) + (defun find-rec2-l (x p n state) + (if (endp x) + (mv nil state) + (mv-let (r state) (find-rec2 (car x) (append p (list n)) state) + (mv-let (r2 state) (find-rec2-l (cdr x) p (1+ n) state) + (mv (append r r2) state)))))) + +(defun expand-def (p x state) + (mv-let (d state) (getdef (usepath p x) state) + (mv-let (x2 err) (rwrite (usepath p x) d) + (mv-let (x3 state) (norm `(or ,@(replace-at p x2 x)) state) + (if (equal (len x3) 1) + (mv t (car x3) state) + (mv nil x state)))))) + +(defun try-paths (l x state) + (if (endp l) + (mv x state) + (mv-let (changed x state) (expand-def (car l) x state) + (if changed + (mv-let (r state) (find-rec2 (usepath (car l) x) (car l) state) + (try-paths (append r (cdr l)) x state)) + (try-paths (cdr l) x state))))) + +(defun expand-defs (x state) + (mv-let (pl state) (find-rec2-l x nil 0 state) + (try-paths (reverse pl) x state))) + +(defun expand-defs-l (x state) + (if (endp x) + (mv nil state) + (mv-let (r state) (expand-defs (car x) state) + (mv-let (r2 state) (expand-defs-l (cdr x) state) + (mv (cons r r2) state))))) + + +(defun norm-lc (x state) + (if (endp x) + (mv nil state) + (mv-let (r state) (norm (car x) state) + (mv-let (r2 state) (norm-lc (cdr x) state) + (mv (append r r2) state))))) + + + + + + +#| + + + +(NIL (TRUE-LISTP X) + (((NOT (CONSP X)) + (TRUE-LISTP (G0 Y X)) + (NOT (TRUE-LISTP (CDR X))) + (NOT (TRUE-LISTP Y)) + (EQUAL (ROT2 (CDR X) + (BINARY-APPEND (BINARY-APPEND (CDR X) Y) + (CONS (CAR X) 'NIL))) + (BINARY-APPEND Y X))) + ((NOT (CONSP X)) + (NOT (EQUAL (ROT2 (CDR X) + (BINARY-APPEND (CDR X) (G0 Y X))) + (BINARY-APPEND (G0 Y X) (CDR X)))) + (NOT (TRUE-LISTP (CDR X))) + (NOT (TRUE-LISTP Y)) + (EQUAL (ROT2 (CDR X) + (BINARY-APPEND (BINARY-APPEND (CDR X) Y) + (CONS (CAR X) 'NIL))) + (BINARY-APPEND Y X))) + ((CONSP X) + X (NOT (TRUE-LISTP Y)) + (EQUAL Y (BINARY-APPEND Y 'NIL)))) + <state>) + +(hl + '(EQUAL (ROT2 (CDR X) + (BINARY-APPEND (BINARY-APPEND (CDR X) Y) + (CONS (CAR X) 'NIL))) + (BINARY-APPEND Y X)) + '(EQUAL (ROT2 (CDR X) + (BINARY-APPEND (CDR X) (G0 Y X))) + (BINARY-APPEND (G0 Y X) (CDR X)))) + +(hl + (BINARY-APPEND (BINARY-APPEND (CDR X) Y) + (CONS (CAR X) 'NIL)) + (BINARY-APPEND (CDR X) (G0 Y X))) + +(hl + '(G1 Y X) + '(BINARY-APPEND Y (CONS (CAR X) 'NIL)) + ) + +(hl + '(BINARY-APPEND (G1 Y X) (CDR X)) + '(BINARY-APPEND Y X) + ) + +|# + + +(defun conp (x state) + (getprop (car x) 'constrainedp nil 'current-acl2-world (w state))) + +(mutual-recursion + (defun constrainedp (x state) + (if (atom x) + nil + (or (conp x state) + (constrainedp-l (cdr x) state)))) + (defun constrainedp-l (x state) + (if (endp x) + nil + (or (constrainedp (car x) state) + (constrainedp-l (cdr x) state))))) + + +(defun pairs (x y) + (if (endp x) + nil + (cons (list (car x) (car y)) + (pairs (cdr x) (cdr y))))) + +(defun try-decomp (x y) + (if (and (consp x) + (consp y) + (equal (car x) (car y))) + (mv nil (pairs (cdr x) (cdr y))) + (mv t nil))) + + +(mutual-recursion + (defun use-subst (x y l) + (if (atom l) + l + (mv-let (r err) (rwrite l `(,x ,y)) + (if err + (use-subst-l x y l) + r)))) + (defun use-subst-l (x y l) + (if (endp l) + nil + (cons (use-subst x y (car l)) + (use-subst-l x y (cdr l)))))) + +(defun rwritel (b x) + (if (endp b) + (mv nil t) + (mv-let (r err) (rwrite x (car b)) + (if err + (rwritel (cdr b) x) + (mv r nil))))) + +(mutual-recursion + (defun use-substl (b l) + (if (atom l) + l + (mv-let (r err) (rwritel b l) + (if err + (use-substl-l b l) + r)))) + (defun use-substl-l (b l) + (if (endp l) + nil + (cons (use-substl b (car l)) + (use-substl-l b(cdr l)))))) + + +(program) + +(defun rm-el (e x) + (if (endp x) + nil + (if (equal e (car x)) + (cdr x) + (cons (car x) (rm-el e (cdr x)))))) + +(defun rm-hyps (hyps x) + (if (endp hyps) + x + (rm-hyps (cdr hyps) (rm-el (car hyps) x)))) + + +(mutual-recursion + (defun find-csub2 (x y e) + (if (atom y) + (mv t y) + (if (equal x y) + (mv nil e) + (mv-let (err cdry) (find-csub2-l x (cdr y) e) + (mv err (cons (car y) cdry)))))) +(defun find-csub2-l (x y e) + (if (endp y) + (mv t nil) + (mv-let (err cary) (find-csub2 x (car y) e) + (if err + (mv-let (err cdry) (find-csub2-l x (cdr y) e) + (mv err (cons (car y) cdry))) + (mv err (cons cary (cdr y)))))))) + +(mutual-recursion + (defun find-csub (x y e) + (if (atom x) + (mv t x y) + (mv-let (err y) (find-csub2 x y e) + (if err + (mv-let (err cdrx y) (find-csub-l (cdr x) y e) + (mv err (cons (car x) cdrx) y)) + (mv err e y))))) + (defun find-csub-l (x y e) + (if (endp x) + (mv t nil y) + (mv-let (err carx y) (find-csub (car x) y e) + (if err + (mv-let (err cdrx y) (find-csub-l (cdr x) y e) + (mv err (cons (car x) cdrx) y)) + (mv err (cons carx (cdr x)) y)))))) + + +(defun gen-common (x) + (let ((a (cadr x)) + (b (caddr x))) + (mv-let (err a b) (find-csub a b 'x0) + `(equal ,a ,b)))) + +(defun orient-eq (x state) + (let ((a (cadr x)) + (b (caddr x))) + (if (and + (consp a) + (conp a state)) + x + `(equal ,b ,a)))) + +(mutual-recursion +(defun replace-consts (x max-var) + (if (atom x) + (mv x max-var) + (if (quotep x) + (let ((max-var (1+ max-var))) + (mv (new-var max-var) max-var)) + (mv-let (r max-var) (replace-consts-l (cdr x) max-var) + (mv (cons (car x) r) max-var))))) +(defun replace-consts-l (x max-var) + (if (endp x) + (mv nil max-var) + (mv-let (r1 max-var) (replace-consts (car x) max-var) + (mv-let (r2 max-var) (replace-consts-l (cdr x) max-var) + (mv (cons r1 r2) max-var)))))) + +; replace any constants on the left side with new variables +(defun gen-unused (x max-var) + (let* ((a (cadr x)) + (b (caddr x)) + ) + (mv-let (r max-var) (replace-consts a max-var) + (mv `(equal ,r ,b) max-var)))) + + +(defun csubstp (d1 state) + (and (consp d1) + (equal (car d1) 'equal) + (consp (cdr d1)) + (consp (cddr d1)) + (let* ( (x (cadr d1)) + (y (caddr d1))) + (or (and + (consp x) + (conp x state)) + (and + (consp y) + (conp y state)))))) + + + ;(access pv (change pv (make pv) :max-fun 1) :max-fun) + + +(mutual-recursion + (defun find-rec-nocon (x state) + (if (atom x) + (mv nil t state) + (if (conp x state) + (mv nil t state) + (mv-let (p err state) (find-rec-nocon-l (cdr x) 1 state) + (if err + (if (recp x state) + (mv nil nil state) + (mv nil t state)) + (mv p nil state)))))) + (defun find-rec-nocon-l (x n state) + (if (endp x) + (mv nil t state) + (mv-let (p err state) (find-rec-nocon (car x) state) + (if err + (find-rec-nocon-l (cdr x) (1+ n) state) + (mv (cons n p) nil state)))))) + + +(defun add-disj2 (d x) + (if (endp x) + nil + (cons + `(case (and ,@(cons d (cdr (cadr (car x))))) ,(caddr (car x))) + (add-disj2 d (cdr x))))) + + ; we assume x is the body of a recursive function which + ; is composed of an if tree with terms at the leaves + ; rl is the list of recursive functions for this + ; body +(defun get-cases12 (x rl) + (if (atom x) + (mv `((case (and) ,x)) 1) + (if (equal (car x) 'if) + (mv-let (c b) (get-cases12 (caddr x) rl) + (mv-let (c2 b2) (get-cases12 (cadddr x) rl) + (if (< b b2) + (mv (append (add-disj2 (cadr x) c2) + (add-disj2 `(not ,(cadr x)) c)) + (+ b b2)) + (mv (append (add-disj2 `(not ,(cadr x)) c) + (add-disj2 (cadr x) c2)) + (+ b b2))))) + (mv `((case (and) ,x)) (if (contains-call rl x) 0 1))))) + +(defun get-cases2 (x rl) + (mv-let (c b) (get-cases12 x rl) (declare (ignore b)) + c)) + +(defun new-clauses2 (p l x) + (if (endp l) + nil + (cons + (append (cdr (cadr (car l))) (replace-at p (caddr (car l)) x)) + (new-clauses2 p (cdr l) x)))) + +(defun str-cat (m s) + (intern (concatenate 'string (symbol-name m) s) "ACL2")) + + +(defmacro simp-term-trans (name args base cond trans) + `(mutual-recursion + (defun ,name ,args + (if (atom ,(car args)) + ,base + (if ,cond + ,trans + (cons (car ,(car args)) (,(str-cat name "-L") (cdr ,(car args)) ,@(cdr args)))))) + (defun ,(str-cat name "-L") ,args + (if (endp ,(car args)) + nil + (cons (,name (car ,(car args)) ,@(cdr args)) + (,(str-cat name "-L") (cdr ,(car args)) ,@(cdr args))))))) + +(simp-term-trans hide-constr (x state) x (conp x state) `(hide ,x)) + +(simp-term-trans rm-hide (x) x (equal (car x) 'hide) (cadr x)) + + +#| + +(hide-constr +'(OR (NOT (CONSP (BINARY-APPEND (CONS X1 'NIL) X2))) + (NOT (TRUE-LISTP X2)) + (NOT (TRUE-LISTP Y)) + (CONSP X2) + (EQUAL (G0 Y (BINARY-APPEND (CONS X1 'NIL) X2)) + (BINARY-APPEND (BINARY-APPEND X2 Y) + (CONS X1 'NIL)))) +state) + + +|# + + +(defun find-csubst (x state) + (if (endp x) + (mv t nil) + (if (csubstp (car x) state) + (mv nil (orient-eq (car x) state)) + (find-csubst (cdr x) state)))) + +; take the clause x and simplify it by locating a +; recursive function and assuming a base case for that +; function +(defun gen-constr (x hyps pv state) + (mv-let (p err state) (find-rec-nocon-l x 0 state) + (if err + (mv t nil pv state) + (mv-let (def state) (getdef (usepath p x) state) + (mv-let (bind err) (pmatch (car def) (usepath p x) nil) + (let* ( + (rn (recp (usepath p x) state)) + (cases (get-cases2 (cadr def) rn)) + (icases (inst-l cases bind))) + ; hide g0? f + (mv-let (err r state) (bash-term-to-dnf `(or ,@hyps ,@(hide-constr-l (car (new-clauses2 p icases x)) state)) nil nil state) (declare (ignore err)) ;elim dtors ? + (if (equal (len r) 1) + (mv-let (err subst) (find-csubst (rm-hide-l (car r)) state) + (if err + (mv t nil pv state) + ;(mv-let (r max-var) (gen-unused (orient-eq subst state) (access pv pv :max-var)) + (mv nil (orient-eq subst state) pv state))) + (mv t nil pv state))))))))) + + + +;(untrace$ bash-term-to-dnf find-csubst gen-unused getdef get-cases1 hide-constr new-clauses2 find-rec-nocon add-disj2 get-cases2) + +;(use-subst '(g x y) '(binary-append (cdr y) (cons (car x) nil)) '((g (cdr x) y))) + +; d is a list of differences that we are trying to resolve +; we are at a base case when one side of an equality is a +; basic constrained function + +(defun remove-nth (n x) + (if (zp n) + (cdr x) + (cons (car x) + (remove-nth (1- n) (cdr x))))) + + + + + + +(defun clausify-diffs (x) + (if (endp x) + nil + (cons `((equal ,(car (car x)) ,(cadr (car x)))) + (clausify-diffs (cdr x))))) + + +(defun gnext (s) + (cons (list (remove-nth (cadr (car s)) (car (car s))) 0) s)) + +(defun bnext (s) + (if (endp s) + nil + (if (< (1+ (cadr (car s))) (len (car (car s)))) + (cons (list (car (car s)) (1+ (cadr (car s)))) (cdr s)) + (bnext (cdr s))))) + +;(gnext '(((1 2) 0) ((0 1 2) 0))) + +;(bnext '(((2) 0) ((1 2) 0) ((0 1 2) 0))) + +(defun trav (s) + (if (endp s) + nil + (if (< 2 (len s)) + (trav (bnext s)) + (trav (gnext s))))) + +;(trav '(((0 1 2) 0))) + + + +(defun cons-calls (l fcall) + (if (endp l) + nil + `(cons ,(inst fcall (car l)) + ,(cons-calls (cdr l) fcall)))) + + + +#| +(mutual-recursion + (defun all-vars (x) + (if (atom x) + (if (constant x) + nil + (list x)) + (if (eq (car x) 'quote) + nil + (all-vars-l (cdr x))))) + (defun all-vars-l (x) + (if (endp x) + nil + (append (all-vars (car x)) + (all-vars-l (cdr x)))))) +|# + +(defun all-terms-c2 (l) + (if (endp l) + nil + (list* (car (car l)) + (cadr (car l)) + (all-terms-c2 (cdr l))))) + +(defun all-terms-c (l) + (if (endp l) + nil + (append (all-terms-c2 (car l)) + (all-terms-c (cdr l))))) + +(defun all-terms-tcs (l) + (if (endp l) + nil + (append (car (car l)) + (all-terms-c (cadr (car l))) + (all-terms-tcs (cdr l))))) + +(defun tcs-to-ifun2 (l fcall) + (if (endp l) + nil + (let ((tests (car (car l))) + (calls (cadr (car l)))) + (cons `((and ,@tests) ,(cons-calls calls fcall)) + (tcs-to-ifun2 (cdr l) fcall))))) + +(mutual-recursion + (defun expand-conses (x al) + (if (atom x) + (if (or (member-equal `(not (endp ,x)) al) + (member-equal `(consp ,x) al)) + `(binary-append (cons (car ,x) 'nil) (cdr ,x)) + x) + (if (quotep x) + x + (if (equal (car x) 'if) + `(if ,(cadr x) + ,(expand-conses (caddr x) (cons (cadr x) al)) + ,(expand-conses (cadddr x) (cons (dumb-negate-lit (cadr x)) al))) + (cons (car x) (expand-conses-l (cdr x) al)))))) + (defun expand-conses-l (x al) + (if (endp x) + nil + (cons (expand-conses (car x) al) + (expand-conses-l (cdr x) al))))) + +(defun cdrs-to-cadrs (x) + (if (endp x) + nil + (cons (list (car (car x)) (cdr (car x))) + (cdrs-to-cadrs (cdr x))))) + +(defun blrewrite (l x) + (if (endp l) + (mv t x) + (let ((lhs (car (car l))) + (rhs (cadr (car l)))) + (mv-let (good bind) (one-way-unify lhs x) + (if (not good) + (blrewrite (cdr l) x) + (mv nil (inst rhs (cdrs-to-cadrs bind)))))))) + +(mutual-recursion + (defun lrewrite (x l) + (if (atom x) + (mv t x) + (if (quotep x) + (mv t x) + (mv-let (err r) (lrewrite-l (cdr x) l) + (mv-let (err r) (blrewrite l (cons (car x) r)) + (if err + (mv t r) + (lrewrite r l))))))) + (defun lrewrite-l (x l) + (if (endp x) + (mv t nil) + (mv-let (err r1) (lrewrite (car x) l) + (mv-let (err r2) (lrewrite-l (cdr x) l) + (mv t (cons r1 r2))))))) + +(defun simp (x r) + (mv-let (err r) (lrewrite x r) r)) + +(defun cond-simp (tbody bind) + (let ((body2 (expand-conses tbody nil))) + (simp (simp body2 bind) `(((cons (car x) (cdr x)) x)) ))) + + +(defun tcs-to-ifun (tcs fn bind state) + (let* ((fmls (all-vars (cons 'dummy (all-terms-tcs tcs)))) + (body (tcs-to-ifun2 tcs (cons fn fmls))) + (body `(cond ,@body))) + (mv-let (err val state) (ld (list `(defun ,fn (,@fmls) nil))) + (mv-let (nop tbody state) (TRANSLATE body nil NIL nil nil (W state) STATE) + (let ((sbody (cond-simp tbody bind))) + (mv-let (err val state) (ld (list (list 'ubt! (list 'quote fn)))) + (mv + `(defun ,fn (,@fmls) + ,sbody) + `(,fn ,@fmls) + state))))))) + + + +; rl must contain err and pv2 and must not contain pv +(defmacro try-ubt (rl call err nerr) + `(let ((nl (new-label (access pv pv :max-label))) + (pv (change pv pv :max-label (1+ (access pv pv :max-label))))) + (mv-let (err val state) (ld (list (list 'deflabel nl))) + (mv-let ,rl ,call + (if err + (let ((pv (change pv pv :max-label (1- (access pv pv :max-label))))) + (mv-let (er val state) (ld (list (list 'ubt! (list 'quote nl)))) + ,err)) + (let ((pv pv2)) + ,nerr)))))) + + +(defun prune-clause (p x state) + (declare (xargs :mode :program)) + (if (endp x) + (mv p state) + (mv-let (err nop state) (refute5 (append p (cdr x)) 6 state) + (if err + (prune-clause (append p (list (car x))) (cdr x) state) + (prune-clause p (cdr x) state))))) + +(defun insert-sorted (a lst) + (if (or (endp lst) + (>= (acl2-count a) (acl2-count (car lst)))) + (cons a lst) + (cons (car lst) (insert-sorted a (cdr lst))))) + +(defun insertion-sort (lst) + (if (endp lst) + lst + (insert-sorted (car lst) (insertion-sort (cdr lst))))) + + + + +(defun find-equal (x) + (if (endp x) + 0 + (if (and (consp (car x)) + (equal (car (car x)) 'equal)) + 0 + (1+ (find-equal (cdr x)))))) + + +(defun tcmp (x y) + (if (atom x) + (if (consp y) + 1 + 0) + (if (atom y) + -1 + (let ((r (tcmp (car x) (car y)))) + (if (equal r 0) + (tcmp (cdr x) (cdr y)) + r))))) + +(defun align-equal (x) + (if (or + (not (consp x)) + (not (equal (car x) 'equal))) + x + (if (< (acl2-count (cadr x)) (acl2-count (caddr x))) + `(equal ,(caddr x) ,(cadr x)) + (if (= (acl2-count (cadr x)) (acl2-count (caddr x))) + (if (equal (tcmp (cadr x) (caddr x)) 1) + `(equal ,(caddr x) ,(cadr x)) + x) + x)))) + +(defun make-rewrite (x) + (let ((disj (cdr x))) + (if (equal (len disj) 1) + (align-equal (car disj)) + (let ((eqd (find-equal disj))) + (let ((eqd (if (equal eqd (len disj)) 0 eqd))) + `(implies + (and + ,@(dumb-negate-lit-lst (remove-nth eqd disj))) + ,(align-equal (nth eqd disj)))))))) + +(defmacro inc-depth (bind call rest) + `(if (< 2 (access pv pv :depth)) + (mv t nil pv state) + (mv-let ,bind + (let ((pv (change pv pv :depth (1+ (access pv pv :depth))))) + ,call) + (let ((pv (change pv pv :depth (1- (access pv pv :depth))))) + ,rest)))) + +(mutual-recursion + (defun match2-0 (d hyps pv state) + (declare (xargs :mode :program)) + (if (endp d) + (mv nil nil pv state) + (let* ((d1 (car d)) + (x (car d1)) + (y (cadr d1))) + (if (and (atom x) + (atom y)) + (if (not (equal x y)) + (mv t nil pv state) + (match2-0 (cdr d) hyps pv state)) + (if (not (constrainedp `(equal ,x ,y) state)) + (mv-let (err r pv state) (prove2 `(equal ,x ,y) pv state) + (if err + (mv t nil pv state) + (match2-0 (cdr d) hyps pv state))) + (if (and + (consp x) + (conp x state)) + (mv-let (err r pv2 state) (match2-0 (use-subst-l x y (cdr d)) hyps (change pv pv :bind (append (access pv pv :bind) (list (list x y)))) state) + (if err + (mv t nil pv state) + (mv nil nil pv2 state))) + (if (and + (consp y) + (conp y state)) + (mv-let (err r pv2 state) (match2-0 (use-subst-l y x (cdr d)) hyps (change pv pv :bind (append (access pv pv :bind) (list (list y x)))) state) + (if err + (mv t nil pv state) + (mv nil nil pv2 state))) + + (mv-let (err r) (try-decomp x y) ; if x and y have the same top function symbol, then decompose them + (if (not err) + (mv-let (err r pv state) (match2-0 (append r (cdr d)) hyps pv state) + (if err + (mv-let (err r pv state) (gen-constr `((equal ,@(car d))) hyps pv state) + (if err + (mv t nil pv state) + (mv-let (err r pv state) + (match2-0 (cons (list (cadr r) (caddr r)) (cdr d)) hyps pv state) + (if err + (mv t r pv state) + (match2-0 (list (use-substl-l (access pv pv :bind) (car d))) hyps pv state))))) + (mv nil r pv state))) + (mv-let (err r pv state) (gen-constr `((equal ,@(car d))) hyps pv state) + (if err + (mv t nil pv state) + (mv-let (err r pv state) + (match2-0 (cons (list (cadr r) (caddr r)) (cdr d)) hyps pv state) + (if err + (mv t r pv state) + (match2-0 (list (use-substl-l (access pv pv :bind) (car d))) hyps pv state)))))))))))))) + +; take an equality and attempt to match it against another disjunct. +; if a match is found, use any bindings present to substitute rhs for lhs +; and return the new y. +; we check that the top symbol of rhs and lhs are the same before attempting a match. + (defun match2-0-fert (x y hyps pv state) + (if (atom y) + (mv t nil pv state) + (mv-let (err r pv state) (match2-0-fert-l x (cdr y) hyps pv state) + (if err + (if (and (consp (cadr x)) ; if the top symbols are equal, attempt a match + (equal (car (cadr x)) + (car y))) + (mv-let (err r pv state) (match2-0 (list (list (cadr x) y)) hyps pv state) + (if err + (mv t nil pv state) + ;replace lhs with rhs in y and attempt to prove new clause + (mv nil (caddr x) pv state))) + (mv t nil pv state)) + (mv nil (cons (car y) r) pv state))))) + + (defun match2-0-fert-l (x y hyps pv state) + (if (endp y) + (mv t nil pv state) + (mv-let (err r pv state) (match2-0-fert x (car y) hyps pv state) + (if err + (mv-let (err r pv state) (match2-0-fert-l x (cdr y) hyps pv state) + (if err + (mv t nil pv state) + (mv nil (cons (car y) r) pv state))) + (mv nil (cons r (cdr y)) pv state))))) + + + + (defun match2 (x y hyps pv state) + (declare (xargs :mode :program)) + (if (or (atom x) (atom y)) + (mv t nil pv state) + (if (equal (car x) 'not) + (if (and (consp (cdr x)) + (equal (car (cadr x)) 'equal)) + (mv-let (err r pv state) (match2-0-fert (cadr x) y hyps pv state) ;we should probably match the eq oriented the other way too + (if err + (mv t nil pv state) + (prove2 (use-substl-l (access pv pv :bind) `(or ,@hyps ,x ,r)) pv state))) + (match2-0 (list (list (cadr x) y)) hyps pv state)) + (if (equal (car y) 'not) + (match2-0 (list (list x (cadr y))) hyps pv state) + (mv t nil pv state))))) + +; i and j are the indices of two disjuncts in clause x +; that we are trying to match against each other + (defun match-l (i j x pv state) + (declare (xargs :mode :program)) + (if (<= (len x) j) + (mv t nil pv state) + (if (or (constrainedp (nth i x) state) + (constrainedp (nth j x) state)) + (try-ubt + (err r pv2 state) + (match2 (nth i x) (nth j x) (remove-nth i (remove-nth j x)) pv state) + (match-l i (1+ j) x pv state) + (mv nil r pv2 state)) + (match-l i (1+ j) x pv state)))) + +; try to prove a clause that has constraints in it by finding +; definitions that allow two disjuncts to match modulo negation. +; cross fertilization is performed if possible. + (defun try-match (i x pv state) + (declare (xargs :mode :program)) + (if (<= (len x) i) + (mv t nil pv state) + (try-ubt + (err r pv2 state) + (match-l i (1+ i) x pv state) + (try-match (1+ i) x pv state) + (mv nil r pv2 state)))) + +(defun induct1 (schemes x pv state) + (declare (xargs :mode :program)) + (if (endp schemes) + (mv t nil pv state) + (try-ubt (err pv2 r tcs state) + (mv-let (err r tcs pv state) (get-induct-goals x (car schemes) pv state) + (mv-let (err r pv state) (prove2 `(and ,@r) pv state) + (mv err pv r tcs state))) + (induct1 (cdr schemes) x pv state) + (let* ((nthm (new-thm (access pv pv :max-thm))) + (pv (change pv pv :max-thm (1+ (access pv pv :max-thm)))) + (ifn (new-ifn (access pv pv :max-ifn))) + (pv (change pv pv :max-ifn (1+ (access pv pv :max-ifn))))) + (mv-let (ifun ifun-call state) (tcs-to-ifun tcs ifn (access pv pv :bind) state) + (let ((xrr (make-rewrite x))) + (let ((ithm `(defthm + ,nthm + ,xrr + :hints + (("Goal" :induct ,ifun-call :do-not-induct t :do-not '(generalize))) + ))) + (mv-let (err val state) (ld (list ifun)) + (if err + (mv (err-fun) r pv state) + (mv-let (err val state) (ld (list ithm)) + (if err + (mv (err-fun) r pv state) + (mv nil + r + (change pv pv :log (append (access pv pv :log) + `(,ifun + ,ithm))) + state)))))))))))) + + (defun ind (x pv state) + (declare (xargs :mode :program)) + (induct1 (get-schemes x state) x pv state)) + +; x is a clause to prove +(defun prove2-0 (x pv state) + (declare (xargs :mode :program)) + (if (constrainedp-l x state) + (try-match 0 x pv state) + (mv-let + (err r state) + (bash-term-to-dnf `(or ,@x) nil nil state) (declare (ignore err)) ;removes tautolgies introduced by constrained defs + (if (null r) + (mv nil t pv state) + (mv-let + (err nop state) + (refute5 x 6 state) + (if err + (mv err nil pv state) +;(inc-depth (err r pv state) +; (ind `(or ,@x) pv state) +; (if err + (mv-let + (x state) + (prune-clause nil (insertion-sort x) state) ;how reliable is prune? used to throw away ih after xfert + + (mv-let + (hit lcl tt pspv) + (generalize-clause2 + x + nil + (change prove-spec-var + (initial-pspv *t* ; term (don't-care) + *t* ; displayed-goal (don't-care) + nil ; otf-flg (don't-care) + (ens state) + (w state) + state + nil) + :pool '((being-proved-by-induction . nil))) + (w state) + state) + (if (equal hit 'hit) + (inc-depth (err r pv state) + (ind `(or ,@(car lcl)) + pv + state) + (if err + (mv err r pv state) + (mv nil r pv state))) + (inc-depth (err r pv state) + (ind `(or ,@x) pv state) + (if err + (mv err r pv state) + (mv nil r pv state)))) + + )))))))) + +; (mv err r pv state)))))) + +; eventually we should change this to try each clause independently and +; generate a list of all possible binding for the constrained functions, +; then try each possibility instead of doing this exponential backtracking +(defun prove2-l (x n pv state) + (declare (xargs :mode :program)) + (if (<= (len x) n) + (if (< 0 (len x)) + (mv t nil pv state) + (mv nil nil pv state)) + (try-ubt (err r pv2 state) + (mv-let (err r pv state) (prove2-0 (nth n x) pv state) + (if err + (mv t nil pv state) + (prove2-l (use-substl-l (access pv pv :bind) (remove-nth n x)) 0 pv state))) + (prove2-l x (1+ n) pv state) + (mv nil nil pv state)))) + + (defun prove2 (x pv state) + (declare (xargs :mode :program)) + (mv-let (err r state) + (bash-term-to-dnf x nil nil state) (declare (ignore err)) + (prove2-l (insertion-sort r) 0 pv state)))) + + +(defmacro bprove (x) + `(encapsulate nil + (set-ignore-ok t) + (set-irrelevant-formals-ok t) + (make-event + (mv-let (err max-fun state) (table bprove 'max-fun) + (mv-let (err max-var state) (table bprove 'max-var) + (mv-let (err max-ifn state) (table bprove 'max-ifn) + (mv-let (err max-thm state) (table bprove 'max-thm) + (mv-let (err max-label state) (table bprove 'max-label) + (mv-let (err r pv state) + (prove2 ',x (make pv :bind nil :schemes nil :log nil :max-fun (or max-fun 0) :max-var (or max-var 0) :max-ifn (or max-ifn 0) :max-thm (or max-thm 0) :max-label (or max-label 0) :depth 0) state) + (mv nil (cons 'progn (append + (list + `(table bprove 'max-fun ,(access pv pv :max-fun)) + `(table bprove 'max-var ,(access pv pv :max-var)) + `(table bprove 'max-ifn ,(access pv pv :max-ifn)) + `(table bprove 'max-thm ,(access pv pv :max-thm)) + `(table bprove 'max-label ,(access pv pv :max-label))) + (access pv pv :log))) state)))))))))) + + + +;(prove2 '(equal (rv1 x 'nil) (rv x)) (make pv :bind nil :schemes nil :log nil :max-fun 0 :max-var 0 :max-ifn 0 :max-thm 0 :max-label 0 :depth 0) state) + +;(GENERALize-clause '((equal (f (rv x)) (g (rv x)))) nil (change prove-spec-var nil :pool '((being-proved-by-induction . nil))) (w state) state) + +;(GENERALize-clause '((equal (f (rv (cons x1 'nil))) (g (rv (cons x1 'nil))))) nil (change prove-spec-var nil :pool '((being-proved-by-induction . nil))) (w state) state) + +;(GENERALize-clause2 '((equal (f (cons x1 'nil)) (g (cons x1 'nil)))) nil (change prove-spec-var nil :pool '((being-proved-by-induction . nil))) (w state) state) + +;(GENERALize-clause2 '((EQUAL (ROT2 X2 (BINARY-APPEND X2 (CONS X1 'NIL))) (BINARY-APPEND (CONS X1 'NIL) X2))) nil (change prove-spec-var nil :pool '((being-proved-by-induction . nil))) (w state) state) + +;(fertilize-clause 0 '((not (equal (f (rv x)) (g (rv x)))) (p (f (rv x)))) nil (change prove-spec-var nil :pool '((being-proved-by-induction . nil))) (w state) state) + + +;(trace$ match2 match2-0 try-match match-l) +;(trace$ bash-term-to-dnf) + +;(trace$ prove2-l prove2-0 ind induct1 get-induct-goals) + +;(trace$ gen-constr try-decomp rm-hyps get-induct-goals) + +;(set-ld-redefinition-action '(:query . :overwrite) state) + +;(set-ld-redefinition-action nil state) + +;(proclaim '(optimize (speed 2) (safety 1) (space 1) (debug 3))) + +(comp t) + +(logic) + + + + +;(prove2 '(implies (and (true-listp x) (true-listp y)) (equal (rot2 x (append x y)) (append y x))) (make pv :bind nil :schemes nil :log nil :max-fun 0 :max-var 0 :max-ifn 0 :max-thm 0 :max-label 0 :depth 0) state) + +;(prove2 '(implies (and (true-listp x)) (equal (rot2 x x) x)) (make pv :bind nil :schemes nil :log nil :max-fun 0 :max-var 0 :max-ifn 0 :max-thm 0 :max-label 0 :depth 0) state) + + +;(prove2 '(equal (ilen x '0) (len x)) (make pv :bind nil :schemes nil :log nil :max-fun 0 :max-var 0 :max-ifn 0 :max-thm 0 :max-label 0 :depth 0) state) + +;fails? +;(prove2 '(equal (rv1 x 'nil) (rv x)) (make pv :bind nil :schemes nil :log nil :max-fun 0 :max-var 0 :max-ifn 0 :max-thm 0 :max-label 0 :depth 0) state) + + + diff --git a/books/workshops/2007/erickson/bprove/refute.lisp b/books/workshops/2007/erickson/bprove/refute.lisp new file mode 100644 index 0000000..a2b69a8 --- /dev/null +++ b/books/workshops/2007/erickson/bprove/refute.lisp @@ -0,0 +1,302 @@ +(in-package "ACL2") + +(include-book "bash") + +#| + +PATH=/projects/hvg/SULFA/linux-bin:$PATH + +/projects/hvg/SULFA/acl2/saved_acl2 + +|# + +;(include-book "/projects/hvg/SULFA/books/sat/sat") +;(include-book "/projects/hvg/SULFA/books/sat/sat-setup") +;(include-book "/projects/hvg/SULFA/books/clause-processors/sat-clause-processor") + + +(defun rv (x) + (if (endp x) + nil + (append (rv (cdr x)) (list (car x))))) + + +(set-state-ok t) + +(defun usepath (p x) + (if (endp p) + x + (usepath (cdr p) (nth (car p) x)))) + +(defun recp (x state) + (getprop (car x) 'recursivep nil 'current-acl2-world (w state))) + + +; find the left innermost recursive term in x +; returns (path err state) +(mutual-recursion + (defun find-rec (x state) + (if (atom x) + (mv nil t state) + (mv-let (p err state) (find-rec-l (cdr x) 1 state) + (if err + (if (recp x state) + (mv nil nil state) + (mv nil t state)) + (mv p nil state))))) + (defun find-rec-l (x n state) + (if (endp x) + (mv nil t state) + (mv-let (p err state) (find-rec (car x) state) + (if err + (find-rec-l (cdr x) (1+ n) state) + (mv (cons n p) nil state)))))) + +(defun find-def (x) + (if (endp x) + nil + (if (equal (car (cadr (car x))) + ':definition) + (car x) + (find-def (cdr x))))) + +(defun getdef (x state) + (let* ((lems + (getprop (car x) 'lemmas nil 'current-acl2-world (w state))) + (def + (find-def lems)) + (body (nth 6 def)) + (fmls (nth 5 def))) + (mv `(,fmls ,body) + state))) + + +(defun bind (pat tgt b) + (let ((a (assoc pat b))) + (if a + (if (equal (cadr a) tgt) + (mv b nil) + (mv nil t)) + (mv (cons (list pat tgt) b) nil)))) + +(defun rep-l (x l) + (if (endp l) + x + (if (equal x (caar l)) + (cadar l) + (rep-l x (cdr l))))) + +(mutual-recursion + (defun inst (tm bind) + (if (atom tm) + (rep-l tm bind) + (if (quotep tm) + tm + (cons (car tm) + (inst-l (cdr tm) bind))))) + (defun inst-l (tm bind) + (if (endp tm) + nil + (cons (inst (car tm) bind) + (inst-l (cdr tm) bind))))) + +(defun inst-ll (l bind) + (if (endp l) + nil + (cons (inst-l (car l) bind) + (inst-ll (cdr l) bind)))) + +(defun constant (x) + (or + (integerp x) + (stringp x) + (characterp x))) + +(mutual-recursion + (defun pmatch (pat tgt b) + (if (atom pat) + (if (constant pat) + (mv b (not (equal pat tgt))) + (mv-let (b err) (bind pat tgt b) + (if err + (mv nil t) + (mv b nil)))) + (if (or (not (consp tgt)) + (not (eq (car pat) (car tgt)))) + (mv nil t) + (if (equal (car pat) 'quote) + (mv b (not (equal (cadr pat) (cadr tgt)))) + (pmatch-l (cdr pat) (cdr tgt) b))))) + (defun pmatch-l (pat tgt b) + (if (endp pat) + (if (eq pat tgt) (mv b nil) (mv nil t)) + (if (endp tgt) + (mv nil t) + (mv-let (b1 err) (pmatch (car pat) (car tgt) b) + (if err + (mv nil t) + (pmatch-l (cdr pat) (cdr tgt) b1))))))) + +(defun rwrite (tm rl) + (let ((lhs (car rl)) + (rhs (cadr rl))) + (mv-let (bind err) (pmatch lhs tm nil) + (if err + (mv nil t) + (mv (inst rhs bind) nil))))) + +(defun add-disj (d x) + (if (endp x) + nil + (cons + (list (cons d (caar x)) (cadar x)) + (add-disj d (cdr x))))) + +(mutual-recursion + (defun contains-call (rl x) + (if (atom x) + nil + (if (member-eq (car x) rl) + t + (contains-call-l rl (cdr x))))) +(defun contains-call-l (rl x) + (if (endp x) + nil + (or (contains-call rl (car x)) + (contains-call-l rl (cdr x)))))) + +; we assume x is the body of a recursive function which +; is composed of an if tree with terms at the leaves +; rl is the list of recursive functions for this +; body +(defun get-cases1 (x rl) + (if (atom x) + (mv (list (list nil x)) 1) + (if (equal (car x) 'if) + (mv-let (c b) (get-cases1 (caddr x) rl) + (mv-let (c2 b2) (get-cases1 (cadddr x) rl) + (if (< b b2) + (mv (append (add-disj (cadr x) c2) + (add-disj `(not ,(cadr x)) c)) + (+ b b2)) + (mv (append (add-disj `(not ,(cadr x)) c) + (add-disj (cadr x) c2)) + (+ b b2))))) + (mv (list (list nil x)) (if (contains-call rl x) 0 1))))) + +(defun get-cases (x rl) + (mv-let (c b) (get-cases1 x rl) (declare (ignore b)) + c)) + +(mutual-recursion + (defun decidable (x state) + (if (atom x) + t + (and + (not (recp x state)) + (decidable-l (cdr x) state)))) + (defun decidable-l (x state) + (if (endp x) + t + (and + (decidable (car x) state) + (decidable-l (cdr x) state))))) + + +(defun replace-at (p nt x) + (if (endp p) + nt + (if (atom x) + x + (update-nth (car p) (replace-at (cdr p) nt (nth (car p) x)) x)))) + + +; l is a list of tuples (c r) where c is a clause and r is the new value +; for x at p under that clause +; we create a new clause that replaces r at p in x for each tuple +(defun new-clauses (p l x) + (if (endp l) + nil + (cons + (append (caar l) (replace-at p (cadar l) x)) + (new-clauses p (cdr l) x)))) + + +#| +(mutual-recursion + (defun refute (x depth sat::$sat state) + (declare (xargs :stobjs sat::$sat :mode :program)) + (if (decidable-l x state) + (acl2::sat x nil sat::$sat state) + (if (zp depth) + (mv nil nil sat::$sat state) + (mv-let (p err state) (find-rec-l x 0 state) (declare (ignore err)) + (mv-let (def state) (getdef (usepath p x) state) + (mv-let (x2 err) (rwrite (usepath p x) def) (declare (ignore err)) + (let ((rn (recp (usepath p x) state))) + (let ((xl (get-cases x2 rn))) + (refute-l (new-clauses p xl x) (1- depth) sat::$sat state))))))))) + (defun refute-l (x depth sat::$sat state) + (declare (xargs :stobjs sat::$sat :mode :program)) + (if (endp x) + (mv nil nil sat::$sat state) + (mv-let (r nop sat::$sat state) + (refute (car x) depth sat::$sat state) (declare (ignore nop)) + (if r + (mv r nil sat::$sat state) + (refute-l (cdr x) depth sat::$sat state)))))) + +(set-ignore-ok t) + + + +(defun refute4 (x depth sat::$sat state) + (declare (xargs :stobjs sat::$sat :mode :program)) + (let ((nop (cw "~x0~%" x))) (declare (ignore nop)) + (refute x depth sat::$sat state))) + +|# + +(mutual-recursion + (defun refute5 (x depth state) + (declare (xargs :mode :program)) + (if (decidable-l x state) + (mv-let (err r state) (bash-term-to-dnf2 `(or ,@x) nil nil state) (declare (ignore err)) + (mv r nil state)) + (if (zp depth) + (mv nil nil state) + (mv-let (p err state) (find-rec-l x 0 state) (declare (ignore err)) + (mv-let (def state) (getdef (usepath p x) state) + (mv-let (x2 err) (rwrite (usepath p x) def) (declare (ignore err)) + (let ((rn (recp (usepath p x) state))) + (let ((xl (get-cases x2 rn))) + (refute5-l (new-clauses p xl x) (1- depth) state))))))))) + (defun refute5-l (x depth state) + (declare (xargs :mode :program)) + (if (endp x) + (mv nil nil state) + (mv-let (r nop state) + (refute5 (car x) depth state) (declare (ignore nop)) + (if r + (mv r nil state) + (refute5-l (cdr x) depth state)))))) + +(defun refute6 (x depth state) + (declare (xargs :mode :program)) + (let ((nop (cw "~x0~%" x))) (declare (ignore nop)) + (refute5 x depth state))) + +(defmacro refute (x) + `(let ((nop (cw "~%ATTEMPTING TO REFUTE~%~%~x0~%~%" ',x))) (declare (ignore nop)) + (mv-let (err r state) + (refute5 (list ',x) 6 state) + (declare (ignore r)) + (if err + (let ((nop (cw "CEX~%~%~x0~%~%REFUTED~%" err))) (declare (ignore nop)) + (mv nil nil state)) + (let ((nop (cw "NO CEX FOUND~%"))) (declare (ignore nop)) + (mv nil nil state)))))) + + + + |