other
(in-package "ACL2")
set-parallel-execution-fnfunction
(defun set-parallel-execution-fn (val ctx state) (declare (xargs :guard (member-eq val '(t nil :bogus-parallelism-ok)))) (cond ((eq (f-get-global 'parallel-execution-enabled state) val) (pprogn (observation ctx "No change in enabling of parallel execution.") (value nil))) (t (er soft ctx "Parallelism can only be enabled in CCL, threaded SBCL, or Lispworks. ~ ~ Additionally, the feature :ACL2-PAR must be set when compiling ~ ACL2 (for example, by using `make' with argument `ACL2_PAR=t'). ~ Either the current Lisp is neither CCL nor threaded SBCL nor ~ Lispworks, or this feature is missing. Consequently, parallelism ~ will remain disabled. Note that you can submit parallelism ~ primitives at the top level when parallel execution is disabled, ~ although they will not result in any parallel execution.~%"))))
set-parallel-executionmacro
(defmacro set-parallel-execution (value) (declare (xargs :guard (member-equal value '(t 't nil 'nil :bogus-parallelism-ok ':bogus-parallelism-ok)))) `(let ((val ,VALUE) (ctx 'set-parallel-execution)) (set-parallel-execution-fn (cond ((consp val) (cadr val)) (t val)) ctx state)))
waterfall-printing-value-for-parallelism-valuefunction
(defun waterfall-printing-value-for-parallelism-value (value) (declare (xargs :guard (member-eq value *waterfall-parallelism-values*))) (cond ((eq value nil) :full) ((eq value :full) :very-limited) ((eq value :top-level) :very-limited) ((eq value :resource-based) :very-limited) ((eq value :resource-and-timing-based) :very-limited) (t (assert$ (eq value :pseudo-parallel) :very-limited))))
print-set-waterfall-parallelism-noticefunction
(defun print-set-waterfall-parallelism-notice (val print-val state) (declare (xargs :guard (and (member-eq val *waterfall-parallelism-values*) (keywordp print-val)))) (let ((str (case val ((nil) "Disabling parallel execution of the waterfall.") (:full "Parallelizing the proof of every subgoal.") (:top-level "Parallelizing the proof of top-level subgoals only.") (:pseudo-parallel "Running the version of the waterfall prepared for parallel ~ execution (stateless). However, we will execute this version of ~ the waterfall serially.") (:resource-and-timing-based "Parallelizing the proof of every subgoal that was determined to ~ take a non-trivial amount of time in a previous proof attempt.") (otherwise "Parallelizing the proof of every subgoal, as long as CPU core ~ resources are available.")))) (observation nil "~@0 Setting waterfall-parallelism to ~s1. Setting ~ waterfall-printing to ~s2 (see :DOC ~ set-waterfall-printing).~%" str (symbol-name val) (symbol-name print-val))))
check-for-no-override-hintsfunction
(defun check-for-no-override-hints (ctx state) (let ((wrld (w state))) (cond ((and (not (cdr (assoc-eq 'hacks-enabled (table-alist 'waterfall-parallelism-table wrld)))) (cdr (assoc-eq :override (table-alist 'default-hints-table wrld)))) (er soft ctx "Before changing the status of waterfall-parallelism, either (1) ~ override hints must be removed from the default-hints-table or (2) ~ waterfall-parallelism hacks must be enabled. (1) can be achieved ~ by calling ~x0. (2) can be achieved by calling ~x1." '(set-override-hints nil) '(set-waterfall-parallelism-hacks-enabled t))) (t (value nil)))))
set-waterfall-parallelism-fnfunction
(defun set-waterfall-parallelism-fn (val ctx state) (cond ((eq val (f-get-global 'waterfall-parallelism state)) (pprogn (observation ctx "Ignoring call to set-waterfall-parallelism since ~ the new value is the same as the current value.~%~%") (value :ignored))) (t (let ((val (if (eq val t) :resource-based val))) (er-progn (cond ((or (null val) (equal val (f-get-global 'waterfall-parallelism state))) (value nil)) (t (check-for-no-override-hints ctx state))) (cond ((member-eq val *waterfall-parallelism-values*) (pprogn (observation ctx "Parallelism can only be enabled in CCL, threaded ~ SBCL, or Lispworks. Additionally, the feature ~ :ACL2-PAR must be set when compiling ACL2 (for ~ example, by using `make' with argument ~ `ACL2_PAR=t'). ~ Either the current Lisp is neither ~ CCL nor threaded SBCL nor Lispworks, or this ~ feature is missing. Consequently, this attempt to ~ set waterfall-parallelism to ~x0 will be ~ ignored.~%~%" val) (value :ignored))) (t (er soft ctx "Illegal value for set-waterfall-parallelism: ~x0. The legal ~ values are ~&1." val *waterfall-parallelism-values*))))))))
set-waterfall-parallelism1macro
(defmacro set-waterfall-parallelism1 (val) `(let* ((val ,VAL) (ctx 'set-waterfall-parallelism)) (er-let* ((val (set-waterfall-parallelism-fn val ctx state))) (cond ((eq val :ignored) (value val)) (t (let ((print-val (waterfall-printing-value-for-parallelism-value val))) (pprogn (print-set-waterfall-parallelism-notice val print-val state) (er-progn (set-waterfall-printing-fn print-val ctx state) (value (list val print-val))))))))))
clearable-memoize-table-entryfunction
(defun clearable-memoize-table-entry (x) (let ((alist (cdr x))) (not (or (cdr (assoc-eq :total alist)) (cdr (assoc-eq :invoke alist))))))
keep-clearable-memoize-table-entriesfunction
(defun keep-clearable-memoize-table-entries (tbl acc) (cond ((endp tbl) (reverse acc)) (t (keep-clearable-memoize-table-entries (cdr tbl) (if (clearable-memoize-table-entry (car tbl)) (cons (car tbl) acc) acc)))))
save-memo-tablemacro
(defmacro save-memo-table nil '(with-output :off (summary event) (table saved-memoize-table nil (keep-clearable-memoize-table-entries (table-alist 'memoize-table world) nil) :clear)))
clear-memo-table-eventsfunction
(defun clear-memo-table-events (alist acc) (declare (xargs :guard (true-list-listp alist))) (cond ((endp alist) acc) (t (clear-memo-table-events (cdr alist) (if (clearable-memoize-table-entry (car alist)) (cons `(table memoize-table ',(CAAR ALIST) nil) acc) acc)))))
clear-memo-tablemacro
(defmacro clear-memo-table nil `(with-output :off (summary event) (make-event (let ((alist (table-alist 'memoize-table (w state)))) (cons 'progn (clear-memo-table-events alist nil))))))
save-and-clear-memoization-settingsmacro
(defmacro save-and-clear-memoization-settings nil '(with-output :off (summary event) (progn (save-memo-table) (clear-memo-table))))
set-memo-table-eventsfunction
(defun set-memo-table-events (alist acc) (declare (xargs :guard (true-list-listp alist))) (cond ((endp alist) acc) (t (set-memo-table-events (cdr alist) (cons `(table memoize-table ',(CAAR ALIST) ',(CDAR ALIST)) acc)))))
restore-memoization-settingsmacro
(defmacro restore-memoization-settings nil `(with-output :off (summary event) (make-event (let ((alist (table-alist 'saved-memoize-table (w state)))) (cons 'progn (set-memo-table-events alist nil))))))
set-waterfall-parallelismmacro
(defmacro set-waterfall-parallelism (val) `(with-output :off (summary event) (make-event (er-let* ((new-val (set-waterfall-parallelism1 ,VAL))) (value (list 'value-triple (list 'quote new-val)))))))
set-waterfall-printing-fnfunction
(defun set-waterfall-printing-fn (val ctx state) (cond ((member-eq val *waterfall-printing-values*) (pprogn (observation ctx "Customizing waterfall printing only makes ~ sense in the #+acl2-par builds of ACL2. ~ Consequently, this attempt to set ~ waterfall-printing to ~x0 will be ignored.~%~%" val) (value :invisible))) (t (er soft ctx "Illegal value for set-waterfall-printing: ~x0. The legal ~ values are ~&1." val *waterfall-printing-values*))))
set-waterfall-printingmacro
(defmacro set-waterfall-printing (val) `(set-waterfall-printing-fn ,VAL 'set-waterfall-printing state))
other
(set-table-guard waterfall-parallelism-table (ttag world) :topic set-waterfall-parallelism-hacks-enabled)
set-waterfall-parallelism-hacks-enabledmacro
(defmacro set-waterfall-parallelism-hacks-enabled (val) (declare (xargs :guard (or (equal val t) (null val)))) `(table waterfall-parallelism-table 'hacks-enabled ,VAL))
set-waterfall-parallelism-hacks-enabled!macro
(defmacro set-waterfall-parallelism-hacks-enabled! (val) `(encapsulate nil (defttag :waterfall-parallelism-hacks) (set-waterfall-parallelism-hacks-enabled ,VAL)))
caar-is-declarepfunction
(defun caar-is-declarep (x) (declare (xargs :guard t)) (and (consp x) (consp (car x)) (eq (caar x) 'declare)))
declare-granularity-pfunction
(defun declare-granularity-p (x) (declare (xargs :guard t)) (and (true-listp x) (eql (length x) 2) (eq (car x) 'declare) (let ((gran-form (cadr x))) (and (true-listp gran-form) (eql (length gran-form) 2) (eq (car gran-form) 'granularity)))))
check-and-parse-for-granularity-formfunction
(defun check-and-parse-for-granularity-form (x) (cond ((not (caar-is-declarep x)) (mv nil nil nil nil x)) ((declare-granularity-p (car x)) (let* ((granularity-declaration (cadar x)) (granularity-form (cadr granularity-declaration))) (mv nil nil t granularity-form (cdr x)))) (t (mv t "Within a parallelism primitive, a granularity form declaration ~ is the only acceptable form of declaration. Some examples of ~ unaccepted declarations are type and ignore declarations. See ~ :DOC granularity." nil nil x))))
pargsmacro
(defmacro pargs (&rest forms) (mv-let (erp msg gran-form-exists gran-form remainder-forms) (check-and-parse-for-granularity-form forms) (cond (erp (er hard 'pargs msg)) ((or (and (equal (length forms) 1) (not gran-form-exists)) (and (equal (length forms) 2) gran-form-exists)) (let ((function-call (car remainder-forms))) (if gran-form-exists `(prog2$ ,GRAN-FORM ,FUNCTION-CALL) function-call))) (t (er hard 'pargs "Pargs was passed the wrong number of arguments. Without a ~ granularity declaration, pargs takes one argument. With a ~ granularity declaration, pargs requires two arguments, the ~ first of which must be of the form ~x0. See :DOC pargs." '(declare (granularity expr)))))))
pletmacro
(defmacro plet (&rest forms) (mv-let (erp msg gran-form-exists gran-form remainder-forms) (check-and-parse-for-granularity-form forms) (cond (erp (er hard 'plet msg)) (gran-form-exists `(prog2$ ,GRAN-FORM (let ,@REMAINDER-FORMS))) (t `(let ,@REMAINDER-FORMS)))))
binary-pandfunction
(defun binary-pand (x y) (declare (xargs :guard t :mode :logic)) (and x y t))
pandmacro
(defmacro pand (&rest forms) (mv-let (erp msg gran-form-exists gran-form remainder-forms) (check-and-parse-for-granularity-form forms) (cond (erp (er hard 'pand msg)) ((atom remainder-forms) t) ((null (cdr remainder-forms)) (list 'if (car remainder-forms) t nil)) (gran-form-exists (list 'prog2$ gran-form (xxxjoin 'binary-pand remainder-forms))) (t (xxxjoin 'binary-pand remainder-forms)))))
binary-porfunction
(defun binary-por (x y) (declare (xargs :guard t :mode :logic)) (if x t (if y t nil)))
pormacro
(defmacro por (&rest forms) (mv-let (erp msg gran-form-exists gran-form remainder-forms) (check-and-parse-for-granularity-form forms) (cond (erp (er hard 'por msg)) ((atom remainder-forms) nil) ((null (cdr remainder-forms)) (list 'if (car remainder-forms) t nil)) (gran-form-exists (list 'prog2$ gran-form (xxxjoin 'binary-por remainder-forms))) (t (xxxjoin 'binary-por remainder-forms)))))
or-listfunction
(defun or-list (x) (declare (xargs :guard (true-listp x) :mode :logic)) (if (endp x) nil (if (car x) t (or-list (cdr x)))))
and-listfunction
(defun and-list (x) (declare (xargs :guard (true-listp x) :mode :logic)) (if (endp x) t (and (car x) (and-list (cdr x)))))
cpu-core-countfunction
(defun cpu-core-count (state) (declare (xargs :stobjs state :guard t)) (mv-let (nullp val state) (read-acl2-oracle state) (declare (ignore nullp)) (mv val state)))
spec-mv-letmacro
(defmacro spec-mv-let (&whole spec-mv-let-form outer-vars computation body) (case-match body ((inner-let inner-vars inner-body ('if test true-branch false-branch)) (cond ((not (member inner-let '(mv-let mv?-let mv-let@par) :test 'eq)) (er hard! 'spec-mv-let "Illegal form (expected inner let to bind with one of ~v0): ~x1. ~ ~ See :doc spec-mv-let." '(mv-let mv?-let mv-let@par) spec-mv-let-form)) ((or (not (symbol-listp outer-vars)) (not (symbol-listp inner-vars)) (intersectp inner-vars outer-vars :test 'eq)) (er hard! 'spec-mv-let "Illegal spec-mv-let form: ~x0. The two bound variable lists ~ must be disjoint true lists of variables, unlike ~x1 and ~x2. ~ See :doc spec-mv-let." spec-mv-let-form inner-vars outer-vars)) (t `(check-vars-not-free (the-very-obscure-future) (mv?-let ,OUTER-VARS ,COMPUTATION (,INNER-LET ,INNER-VARS ,INNER-BODY (cond ((check-vars-not-free ,OUTER-VARS ,TEST) ,TRUE-BRANCH) (t (check-vars-not-free ,OUTER-VARS ,FALSE-BRANCH))))))))) (& (er hard! 'spec-mv-let "Illegal form, ~x0. See :doc spec-mv-let." spec-mv-let-form))))
set-total-parallelism-work-limit-fnfunction
(defun set-total-parallelism-work-limit-fn (val state) (declare (xargs :guard (or (equal val :none) (integerp val)))) (f-put-global 'total-parallelism-work-limit val state))
set-total-parallelism-work-limitmacro
(defmacro set-total-parallelism-work-limit (val) (declare (xargs :guard (or (equal val :none) (integerp val)))) `(set-total-parallelism-work-limit-fn ,VAL state))
set-total-parallelism-work-limit-error-fnfunction
(defun set-total-parallelism-work-limit-error-fn (val state) (declare (xargs :guard (or (equal val t) (null val)))) (f-put-global 'total-parallelism-work-limit-error val state))
set-total-parallelism-work-limit-errormacro
(defmacro set-total-parallelism-work-limit-error (val) (declare (xargs :guard (or (equal val t) (null val)))) `(set-total-parallelism-work-limit-error-fn ,VAL state))