← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2006/hunt-reeber/support/sat.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/2006/hunt-reeber/support/sat.lisp
 
1
 
 
2
(in-package "ACL2")
 
3
 
 
4
;; (include-book "/projects/hvg/SULFA/books/sat/sat")
 
5
 
 
6
;; This file contains the examples from our paper that we
 
7
;; were able to prove using our SAT based hint.
 
8
;; The theorems are given in block comments, since our
 
9
;; SAT extension is not available without modifying the 
 
10
;; ACL2 source code.
 
11
 
 
12
;; For a description of the example and a description of
 
13
;; how this relates to our SAT system see our workshop paper,
 
14
;; A SAT-Based Procedure for Verifying Finite State Machines in ACL2.
 
15
 
 
16
(defun n-bleq (n x y)
 
17
  (if (zp n)
 
18
      t
 
19
    (and (iff (car x) (car y))
 
20
         (n-bleq (1- n) (cdr x) (cdr y)))))
 
21
 
 
22
(defun xor3 (x y z)
 
23
  (xor x (xor y z)))
 
24
 
 
25
(defun maj3 (x y z)
 
26
  (if x (or y z)
 
27
    (and y z)))
 
28
 
 
29
;; Returns a n+1 length sum of the first
 
30
;; n bits of a and b (plus the carray).
 
31
(defun v-adder (n c a b)
 
32
  (if (zp n)
 
33
      (list c)
 
34
    (cons (xor3 c (car a) (car b))
 
35
          (v-adder (1- n) 
 
36
                   (maj3 c (car a) (car b))
 
37
                   (cdr a) (cdr b)))))
 
38
 
 
39
;; 4 Bit Adder Associativity
 
40
;; (thm 
 
41
;;   (n-bleq 4 (v-adder 4 nil (v-adder 4 nil a b) c)
 
42
;;           (v-adder 4 nil a (v-adder 4 nil b c)))
 
43
;;   :hints (("Goal" :external (sat nil sat::$sat))))
 
44
 
 
45
;; 32 bit adder associativity
 
46
;; (thm 
 
47
;;  (n-bleq 32 (v-adder 32 nil (v-adder 32 nil a b) c)
 
48
;;          (v-adder 32 nil a (v-adder 32 nil b c)))
 
49
;;  :hints (("Goal" :external (sat nil sat::$sat))))
 
50
 
 
51
;; 200 Bit adder associativity
 
52
;; (thm 
 
53
;;  (n-bleq 200 (v-adder 200 nil (v-adder 200 nil a b) c)
 
54
;;          (v-adder 200 nil a (v-adder 200 nil b c)))
 
55
;;   :hints (("Goal" :external (sat nil sat::$sat))))
 
56
 
 
57
(defun nth-cdr (n x)
 
58
  (if (zp n)
 
59
      x
 
60
    (nth-cdr (1- n) (cdr x))))
 
61
 
 
62
(defun nth-sublist (n lst)
 
63
  (if (zp n)
 
64
      nil
 
65
    (cons (car lst) (nth-sublist (1- n) (cdr lst)))))
 
66
 
 
67
(defun append-n (n x y)
 
68
  (if (zp n)
 
69
      y
 
70
    (cons (car x) (append-n (1- n) (cdr x) y))))
 
71
 
 
72
(defun n-nills (n)
 
73
  (if (zp n)
 
74
      nil
 
75
    (cons nil (n-nills (1- n)))))
 
76
 
 
77
(defun rev-n (n x ans)
 
78
  (if (zp n)
 
79
      ans
 
80
    (rev-n (1- n) (cdr x) (cons (car x) ans))))
 
81
 
 
82
(defun mux-n-help (n in rsel)
 
83
  (if (zp n)
 
84
      (car in)
 
85
    (if (car rsel)
 
86
        (mux-n-help (1- n) (nth-cdr (expt 2 (1- n)) in) (cdr rsel))
 
87
      (mux-n-help (1- n) in (cdr rsel)))))
 
88
 
 
89
(defun mux-n (n in sel)
 
90
  (mux-n-help n in (rev-n n sel nil)))
 
91
 
 
92
(defun mux-n-w-help (n w in)
 
93
  (if (zp n)
 
94
      nil
 
95
    (cons (car in) (mux-n-w-help (1- n) w (nth-cdr w in)))))
 
96
 
 
97
(defun mux-n-w1 (nw sn w in sel)
 
98
  (if (zp nw)
 
99
      nil
 
100
    (cons (mux-n sn (mux-n-w-help (expt 2 sn) w in) sel)
 
101
          (mux-n-w1 (1- nw) sn w (cdr in) sel))))
 
102
 
 
103
(defun mux-n-w (n w in sel)
 
104
  (mux-n-w1 w n w in sel))
 
105
 
 
106
(defun shift-mux-help (n w reg)
 
107
  (if (zp n)
 
108
      nil
 
109
    (append-n w reg (shift-mux-help (1- n) w (cons nil reg)))))
 
110
 
 
111
(defun shifter (sn rn rshift reg)
 
112
  (if (zp sn)
 
113
      reg
 
114
    (mux-n-w sn rn (shift-mux-help (expt 2 sn) rn reg) rshift)))
 
115
 
 
116
;; 32x6 Shift-0
 
117
;; (thm 
 
118
;;  (implies 
 
119
;;   (car (nth-cdr 5 shift0))
 
120
;;   (n-bleq 32 
 
121
;;           (shifter 6 32 shift0 reg)
 
122
;;           (n-nills 32)))
 
123
;;   :hints (("Goal" :external (sat nil sat::$sat))))
 
124
 
 
125
;; 64x7 Shift-0
 
126
;; (thm 
 
127
;;  (implies 
 
128
;;   (car (nth-cdr 6 shift0))
 
129
;;   (n-bleq 64 (shifter 7 64 shift0 reg)
 
130
;;           (n-nills 64)))
 
131
;;   :hints (("Goal" :external (sat nil sat::$sat))))
 
132
 
 
133
;; 32x4 Add-shift
 
134
;; (thm
 
135
;;  (n-bleq 32 
 
136
;;          (shifter 4 32 shift0 (shifter 4 32 shift1 reg))
 
137
;;          (shifter 5 32 (v-adder 4 nil shift0 shift1) reg))
 
138
;;   :hints (("Goal" :external (sat nil sat::$sat))))
 
139
 
 
140
;; 64x6 Add-shift
 
141
;; (thm
 
142
;;  (n-bleq 64 
 
143
;;          (shifter 6 64 shift0 (shifter 6 64 shift1 reg))
 
144
;;          (shifter 7 64 (v-adder 6 nil shift0 shift1) reg))
 
145
;;   :hints (("Goal" :external (sat nil sat::$sat))))
 
146
 
 
147
(defun increment (n x)
 
148
  (if (zp n)
 
149
      nil
 
150
    (if (car x)
 
151
        (cons nil (increment (1- n) (cdr x)))
 
152
      (cons t (cdr x)))))
 
153
 
 
154
(defun next_digit_counter_state (x)
 
155
  (if (n-bleq 4 x '(t nil nil t))
 
156
      (list '(nil nil nil nil) t)
 
157
    (list (increment 4 x) nil)))
 
158
 
 
159
(defun next_counter_state (n x)
 
160
  (let* ((curr_d_out (next_digit_counter_state (car x)))
 
161
         (curr_d_val (car curr_d_out))
 
162
         (curr_d_reset (cadr curr_d_out)))
 
163
    (if (zp n)
 
164
        nil
 
165
      (if curr_d_reset
 
166
          (cons curr_d_val (next_counter_state (1- n) (cdr x)))
 
167
        (cons curr_d_val (cdr x))))))
 
168
 
 
169
(defun valid_digit (a)
 
170
  (let ((a1 (cadr a))
 
171
        (a2 (caddr a))
 
172
        (a3 (cadddr a)))
 
173
    (not (and a3 (or a2 a1)))))
 
174
 
 
175
(defun valid_digits (n x)
 
176
  (if (zp n)
 
177
      (not (consp x))
 
178
    (and (valid_digit (car x))
 
179
         (valid_digits (1- n) (cdr x)))))
 
180
 
 
181
;; 100 Digit Counter Invariant
 
182
;; (thm
 
183
;;  (implies
 
184
;;   (valid_digits 100 x)
 
185
;;   (valid_digits 100 (next_counter_state 100 x)))
 
186
;;   :hints (("Goal" :external (sat nil sat::$sat))))