← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2007/erickson/bprove/refute.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2007/erickson/bprove/refute.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(include-book "bash")
 
4
 
 
5
#|
 
6
 
 
7
PATH=/projects/hvg/SULFA/linux-bin:$PATH
 
8
 
 
9
/projects/hvg/SULFA/acl2/saved_acl2
 
10
 
 
11
|#
 
12
 
 
13
;(include-book "/projects/hvg/SULFA/books/sat/sat")
 
14
;(include-book "/projects/hvg/SULFA/books/sat/sat-setup")
 
15
;(include-book "/projects/hvg/SULFA/books/clause-processors/sat-clause-processor")
 
16
 
 
17
 
 
18
(defun rv (x)
 
19
  (if (endp x)
 
20
      nil
 
21
    (append (rv (cdr x)) (list (car x)))))
 
22
 
 
23
 
 
24
(set-state-ok t)
 
25
 
 
26
(defun usepath (p x)
 
27
  (if (endp p)
 
28
      x
 
29
    (usepath (cdr p) (nth (car p) x))))
 
30
 
 
31
(defun recp (x state)
 
32
  (getprop (car x) 'recursivep nil 'current-acl2-world (w state)))
 
33
 
 
34
 
 
35
; find the left innermost recursive term in x
 
36
; returns (path err state)
 
37
(mutual-recursion
 
38
 (defun find-rec (x state)
 
39
  (if (atom x)
 
40
      (mv nil t state)
 
41
    (mv-let (p err state) (find-rec-l (cdr x) 1 state)
 
42
            (if err
 
43
                (if (recp x state)
 
44
                    (mv nil nil state)
 
45
                  (mv nil t state))
 
46
              (mv p nil state)))))
 
47
 (defun find-rec-l (x n state)
 
48
   (if (endp x)
 
49
       (mv nil t state)
 
50
     (mv-let (p err state) (find-rec (car x) state)
 
51
             (if err
 
52
                 (find-rec-l (cdr x) (1+ n) state)
 
53
               (mv (cons n p) nil state))))))
 
54
 
 
55
(defun find-def (x)
 
56
  (if (endp x)
 
57
      nil
 
58
    (if (equal (car (cadr (car x)))
 
59
               ':definition)
 
60
        (car x)
 
61
      (find-def (cdr x)))))
 
62
 
 
63
(defun getdef (x state)
 
64
  (let* ((lems
 
65
          (getprop (car x) 'lemmas nil 'current-acl2-world (w state)))
 
66
         (def
 
67
          (find-def lems))
 
68
         (body (nth 6 def))
 
69
         (fmls (nth 5 def)))
 
70
          (mv `(,fmls ,body)
 
71
              state)))
 
72
 
 
73
 
 
74
(defun bind (pat tgt b)
 
75
  (let ((a (assoc pat b)))
 
76
    (if a
 
77
        (if (equal (cadr a) tgt)
 
78
            (mv b nil)
 
79
          (mv nil t))
 
80
      (mv (cons (list pat  tgt) b) nil))))
 
81
 
 
82
(defun rep-l (x l)
 
83
  (if (endp l)
 
84
      x
 
85
    (if (equal x (caar l))
 
86
        (cadar l)
 
87
      (rep-l x (cdr l)))))
 
88
 
 
89
(mutual-recursion
 
90
 (defun inst (tm bind)
 
91
   (if (atom tm)
 
92
       (rep-l tm bind)
 
93
     (if (quotep tm)
 
94
         tm
 
95
       (cons (car tm)
 
96
             (inst-l (cdr tm) bind)))))
 
97
 (defun inst-l (tm bind)
 
98
   (if (endp tm)
 
99
       nil
 
100
     (cons (inst (car tm) bind)
 
101
           (inst-l (cdr tm) bind)))))
 
102
 
 
103
(defun inst-ll (l bind)
 
104
  (if (endp l)
 
105
      nil
 
106
    (cons (inst-l (car l) bind)
 
107
          (inst-ll (cdr l) bind))))
 
108
 
 
109
(defun constant (x)
 
110
  (or
 
111
   (integerp x)
 
112
   (stringp x)
 
113
   (characterp x)))
 
114
 
 
115
(mutual-recursion
 
116
 (defun pmatch (pat tgt b)
 
117
   (if (atom pat)
 
118
       (if (constant pat)
 
119
           (mv b (not (equal pat tgt)))
 
120
         (mv-let (b err) (bind pat tgt b)
 
121
                 (if err
 
122
                     (mv nil t)
 
123
                   (mv b nil))))
 
124
     (if (or (not (consp tgt))
 
125
             (not (eq (car pat) (car tgt))))
 
126
         (mv nil t)
 
127
       (if (equal (car pat) 'quote)
 
128
           (mv b (not (equal (cadr pat) (cadr tgt))))
 
129
         (pmatch-l (cdr pat) (cdr tgt) b)))))
 
130
 (defun pmatch-l (pat tgt b)
 
131
   (if (endp pat)
 
132
       (if (eq pat tgt) (mv b nil) (mv nil t))
 
133
     (if (endp tgt)
 
134
         (mv nil t)
 
135
       (mv-let (b1 err) (pmatch (car pat) (car tgt) b)
 
136
               (if err
 
137
                   (mv nil t)
 
138
                 (pmatch-l (cdr pat) (cdr tgt) b1)))))))
 
139
 
 
140
(defun rwrite (tm rl)
 
141
  (let ((lhs (car rl))
 
142
        (rhs (cadr rl)))
 
143
    (mv-let (bind err) (pmatch lhs tm nil)
 
144
            (if err
 
145
                (mv nil t)
 
146
              (mv (inst rhs bind) nil)))))
 
147
 
 
148
(defun add-disj (d x)
 
149
  (if (endp x)
 
150
      nil
 
151
    (cons
 
152
     (list (cons d (caar x)) (cadar x))
 
153
     (add-disj d (cdr x)))))
 
154
 
 
155
(mutual-recursion
 
156
 (defun contains-call (rl x)
 
157
  (if (atom x)
 
158
      nil
 
159
    (if (member-eq (car x) rl)
 
160
        t
 
161
      (contains-call-l rl (cdr x)))))
 
162
(defun contains-call-l (rl x)
 
163
  (if (endp x)
 
164
      nil
 
165
    (or (contains-call rl (car x))
 
166
        (contains-call-l rl (cdr x))))))
 
167
   
 
168
; we assume x is the body of a recursive function which  
 
169
; is composed of an if tree with terms at the leaves
 
170
; rl is the list of recursive functions for this 
 
171
; body
 
172
(defun get-cases1 (x rl)
 
173
  (if (atom x)
 
174
      (mv (list (list nil x)) 1)
 
175
    (if (equal (car x) 'if)
 
176
        (mv-let (c b) (get-cases1 (caddr x) rl)
 
177
                (mv-let (c2 b2) (get-cases1 (cadddr x) rl)
 
178
                        (if (< b b2)
 
179
                            (mv (append         (add-disj (cadr x) c2)
 
180
                                                (add-disj `(not ,(cadr x)) c))
 
181
                                (+ b b2))
 
182
                          (mv (append (add-disj `(not ,(cadr x)) c)
 
183
                                        (add-disj (cadr x) c2))
 
184
                                (+ b b2)))))
 
185
      (mv (list (list nil x)) (if (contains-call rl x) 0 1)))))
 
186
 
 
187
(defun get-cases (x rl)
 
188
  (mv-let (c b) (get-cases1 x rl) (declare (ignore b))
 
189
          c))
 
190
    
 
191
(mutual-recursion
 
192
 (defun decidable (x state)
 
193
  (if (atom x)
 
194
      t
 
195
    (and
 
196
     (not (recp x state))
 
197
     (decidable-l (cdr x) state))))
 
198
 (defun decidable-l (x state)
 
199
   (if (endp x)
 
200
       t
 
201
     (and
 
202
      (decidable (car x) state)
 
203
      (decidable-l (cdr x) state)))))
 
204
 
 
205
 
 
206
(defun replace-at (p nt x)
 
207
  (if (endp p)
 
208
      nt
 
209
    (if (atom x)
 
210
        x
 
211
      (update-nth (car p) (replace-at (cdr p) nt (nth (car p) x)) x))))
 
212
 
 
213
 
 
214
; l is a list of tuples (c r) where c is a clause and r is the new value
 
215
; for x at p under that clause
 
216
; we create a new clause that replaces r at p in x for each tuple
 
217
(defun new-clauses (p l x)
 
218
  (if (endp l)
 
219
      nil
 
220
    (cons
 
221
     (append (caar l) (replace-at p (cadar l) x))
 
222
     (new-clauses p (cdr l) x))))
 
223
  
 
224
 
 
225
#|
 
226
(mutual-recursion
 
227
 (defun refute (x depth sat::$sat state)
 
228
  (declare (xargs :stobjs sat::$sat :mode :program))
 
229
  (if (decidable-l x state)
 
230
      (acl2::sat x nil sat::$sat state)
 
231
    (if (zp depth)
 
232
        (mv nil nil sat::$sat state) 
 
233
      (mv-let (p err state) (find-rec-l x 0 state) (declare (ignore err))
 
234
              (mv-let (def state) (getdef (usepath p x) state)
 
235
                      (mv-let (x2 err) (rwrite (usepath p x) def) (declare (ignore err))
 
236
                              (let ((rn (recp (usepath p x) state)))
 
237
                                      (let ((xl (get-cases x2 rn)))
 
238
                                        (refute-l (new-clauses p xl x) (1- depth) sat::$sat state)))))))))
 
239
 (defun refute-l (x depth sat::$sat state)
 
240
     (declare (xargs :stobjs sat::$sat :mode :program))
 
241
   (if (endp x)
 
242
       (mv nil nil sat::$sat state)
 
243
     (mv-let (r nop sat::$sat state) 
 
244
             (refute (car x) depth sat::$sat state)  (declare (ignore nop))
 
245
             (if r
 
246
                 (mv r nil sat::$sat state)
 
247
               (refute-l (cdr x) depth sat::$sat state))))))
 
248
 
 
249
(set-ignore-ok t)
 
250
 
 
251
 
 
252
 
 
253
(defun refute4 (x depth sat::$sat state)
 
254
  (declare (xargs :stobjs sat::$sat :mode :program))
 
255
  (let ((nop (cw "~x0~%" x))) (declare (ignore nop))
 
256
       (refute x depth sat::$sat state)))
 
257
 
 
258
|#
 
259
 
 
260
(mutual-recursion
 
261
 (defun refute5 (x depth  state)
 
262
   (declare (xargs  :mode :program))
 
263
  (if (decidable-l x state)
 
264
      (mv-let (err r state) (bash-term-to-dnf2 `(or ,@x) nil nil state) (declare (ignore err))
 
265
              (mv r nil  state))
 
266
    (if (zp depth)
 
267
        (mv nil nil  state) 
 
268
      (mv-let (p err state) (find-rec-l x 0 state) (declare (ignore err))
 
269
              (mv-let (def state) (getdef (usepath p x) state)
 
270
                      (mv-let (x2 err) (rwrite (usepath p x) def) (declare (ignore err))
 
271
                              (let ((rn (recp (usepath p x) state)))
 
272
                                      (let ((xl (get-cases x2 rn)))
 
273
                                        (refute5-l (new-clauses p xl x) (1- depth)  state)))))))))
 
274
 (defun refute5-l (x depth  state)
 
275
     (declare (xargs  :mode :program))
 
276
   (if (endp x)
 
277
       (mv nil nil  state)
 
278
     (mv-let (r nop  state) 
 
279
             (refute5 (car x) depth  state)  (declare (ignore nop))
 
280
             (if r
 
281
                 (mv r nil  state)
 
282
               (refute5-l (cdr x) depth  state))))))
 
283
 
 
284
(defun refute6 (x depth  state)
 
285
  (declare (xargs  :mode :program))
 
286
  (let ((nop (cw "~x0~%" x))) (declare (ignore nop))
 
287
       (refute5 x depth  state)))
 
288
 
 
289
(defmacro refute (x)
 
290
 `(let ((nop (cw "~%ATTEMPTING TO REFUTE~%~%~x0~%~%" ',x))) (declare (ignore nop))
 
291
  (mv-let (err r state) 
 
292
           (refute5 (list ',x) 6 state)
 
293
           (declare (ignore r))
 
294
           (if err
 
295
               (let ((nop (cw "CEX~%~%~x0~%~%REFUTED~%" err))) (declare (ignore nop))
 
296
                 (mv nil nil state))
 
297
             (let ((nop (cw "NO CEX FOUND~%"))) (declare (ignore nop))
 
298
               (mv nil nil  state))))))
 
299
 
 
300
 
 
301
 
 
302