← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/tutorial/boothmul.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/centaur/tutorial/boothmul.lisp
65
65
(value-triple (set-max-mem (* 3 (expt 2 30))))
66
66
(value-triple (tshell-ensure))
67
67
 
68
 
(make-event
69
 
 
70
 
; Disabling waterfall parallelism for unknown reasons other than that
71
 
; certification stalls out with it enabled.
72
 
 
73
 
 (if (and (hons-enabledp state)
74
 
          (f-get-global 'parallel-execution-enabled state))
75
 
     (er-progn (set-waterfall-parallelism nil)
76
 
               (value '(value-triple nil)))
77
 
   (value '(value-triple nil))))
78
 
 
79
68
 
80
69
; Setup.  This should be familiar if you've looked at, e.g., the alu16
81
70
; tutorial.
509
498
            ;; Need to know that the intermediate values are non-X:
510
499
            :use ((:instance boothmul-pps-types))
511
500
            :in-theory (stv-decomp-theory)))))
512
 
|#
 
501
 
513
502
 
514
503
; For reference, here is the same decomposition lemma, but proven using GL
515
504
; instead of the specialized theory:
533
522
 
534
523
(local (in-theory (disable boothmul-decomp-is-boothmul-via-GL)))
535
524
 
 
525
|#
 
526
 
 
527
 
536
528
; All that remains is to chain the above facts together.
537
529
;
538
530
;   1. By this last GL lemma, we know how to express the result of