← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/aig/count-branches-fast.lsp

  • 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/centaur/aig/count-branches-fast.lsp
 
1
 
 
2
#+hons
 
3
(progn
 
4
 
 
5
  (defparameter *count-branches-to-memo-table*
 
6
    (hl-mht))
 
7
 
 
8
  (defun count-branches-to (x n)
 
9
    (labels
 
10
        ((count-branches-to1
 
11
          (x)
 
12
          (let* ((max (* 2 n))
 
13
                 (ar (make-array max))
 
14
                 (avrc (cons nil nil))
 
15
                 (cnt 0))
 
16
            (declare (type (simple-array t (*)) ar)
 
17
                     (dynamic-extent ar))
 
18
            (labels
 
19
                ((outer (x)
 
20
                        (labels
 
21
                            ((fn (x)
 
22
                                 (cond
 
23
                                  ((atom x) nil)
 
24
                                  ((eq (car x) avrc) nil)
 
25
                                  ((eq (car x) (cdr x))
 
26
                                   (fn (cdr x)))
 
27
                                  (t (setf (aref ar cnt) x)
 
28
                                     (setf
 
29
                                      (aref ar
 
30
                                            (the fixnum (+ 1 cnt)))
 
31
                                      (car x))
 
32
                                     (setq cnt (the fixnum (+ 2 cnt)))
 
33
                                     (if (>= cnt max)
 
34
                                         (return-from outer nil))
 
35
                                     (fn (car x))
 
36
                                     (fn (cdr x))
 
37
                                     (rplaca (the cons x) avrc)))))
 
38
                          (fn x))))
 
39
              (unwind-protect
 
40
                  (progn
 
41
                    (outer x)
 
42
                    (values (if (>= cnt max)
 
43
                                nil
 
44
                              (floor cnt 2))))
 
45
                (loop for i fixnum below cnt by 2 do
 
46
                      (rplaca (the cons (aref ar i))
 
47
                              (aref ar (the fixnum (+ i 1)))))))))
 
48
         (lookup
 
49
          (x)
 
50
          (when (not *count-branches-to-memo-table*)
 
51
            (setq *count-branches-to-memo-table* (hl-mht)))
 
52
          (b* (((mv ans present)
 
53
                (gethash x *count-branches-to-memo-table*)))
 
54
            (if present
 
55
                (if (car ans)
 
56
                    (if (<= (cdr ans) n)
 
57
                        (mv (cdr ans) t)
 
58
                      (mv nil t))
 
59
                  (if (>= (cdr ans) n)
 
60
                      (mv nil t)
 
61
                    (mv nil nil)))
 
62
              (mv nil nil))))
 
63
         (descend
 
64
          (x)
 
65
          (cond ((atom x) x)
 
66
                ((eq (car x) (cdr x))
 
67
                 (descend (car x)))
 
68
                (t x))))
 
69
      (b* ((x (hons-copy x))
 
70
           ((mv ans ok)
 
71
            (lookup x)))
 
72
        (if ok
 
73
            ans
 
74
          (b* ((dx (descend x))
 
75
               ((mv ans ok)
 
76
                (lookup dx)))
 
77
            (if ok
 
78
                ans
 
79
              (let* ((ans
 
80
                      (count-branches-to1 dx))
 
81
                     (mem (if ans (cons t ans) (cons nil n))))
 
82
                (setf (gethash x *count-branches-to-memo-table*) mem)
 
83
                (setf (gethash dx *count-branches-to-memo-table*) mem)
 
84
                ans)))))))
 
85
 
 
86
  ;; BOZO really profile this?
 
87
 
 
88
  (mf-note-arity 'count-branches-to 2 1)
 
89
 
 
90
  (profile-fn 'count-branches-to)
 
91
 
 
92
  #+Clozure
 
93
  ;; Dirty hack so as to clear the count-branches-to memoize table whenever
 
94
  ;; clearing the other memoize tables.  BOZO is this something we need to do?
 
95
  (setf (gethash 'count-branches-to *memoize-info-ht*)
 
96
        (change memoize-info-ht-entry
 
97
                (gethash 'count-branches-to *memoize-info-ht*)
 
98
                :tablename '*count-branches-to-memo-table*))
 
99
  )