Notes about the optimization of bitset-members.
(ttag-bitset-members x) → *
The basic version of
We found this wasn't very efficient in 64-bit CCL, and have developed an alternate implementation that uses:
Basic performance testing suggests that
(include-book "bitsets") (include-book "centaur/aig/random-sim" :dir :system) (include-book "centaur/misc/memory-mgmt" :dir :system) (include-book "std/util/defconsts" :dir :system) (acl2::set-max-mem ;; newline to fool dependency scanner (* 30 (expt 2 30))) (acl2::defconsts (*random-data* state) (acl2::random-list 100000 (ash 1 5000) state)) (defund bitset-members-list (x) (if (atom x) nil (cons (bitset-members (car x)) (bitset-members-list (cdr x))))) (defund ttag-bitset-members-list (x) (if (atom x) nil (cons (ttag-bitset-members (car x)) (ttag-bitset-members-list (cdr x))))) (progn$ (gc$) (time$ (bitset-members-list *random-data*) :msg "Unoptimized Original: ~st sec, ~sa bytes~%") (gc$) (time$ (ttag-bitset-members-list *random-data*) :msg "Unoptimized TTAG: ~st sec, ~sa bytes~%") nil) (include-book "bitsets-opt") (progn$ (gc$) (time$ (bitset-members-list *random-data*) :msg "Optimized Original: ~st sec, ~sa bytes~%") (gc$) (time$ (ttag-bitset-members-list *random-data*) :msg "Optimized TTAG: ~st sec, ~sa bytes~%") nil)
And the results (on compute-1-3):
Unoptimized Original: 12.80 sec, 4,001,843,488 bytes Unoptimized TTAG: 8.27 sec, 9,118,511,648 bytes Optimized Original: 4.05 sec, 4,001,843,488 bytes Optimized TTAG: 4.01 sec, 4,001,843,488 bytes
Function:
(defun ttag-bitset-members-aux (slice x acc) (declare (xargs :guard (and (natp slice) (integerp x)))) (if (zp slice) (bits-0-31 (ash slice 5) (bignum-extract x slice) acc) (ttag-bitset-members-aux (the (integer 0 *) (- (lnfix slice) 1)) x (bits-0-31 (the (integer 0 *) (ash slice 5)) (bignum-extract x slice) acc))))
Theorem:
(defthm ttag-bitset-members-aux-redef (implies (and (natp slice) (integerp x)) (equal (ttag-bitset-members-aux slice x acc) (append (bits-between 0 (* (+ 1 slice) 32) x) acc))))
Function:
(defun ttag-bitset-members (x) (declare (xargs :guard (natp x))) (let ((__function__ 'ttag-bitset-members)) (declare (ignorable __function__)) (mbe :logic (bitset-members x) :exec (ttag-bitset-members-aux (the (integer 0 *) (ash (integer-length x) -5)) x nil))))