[acl2/acl2] 7086e8: [bv] Drop unneeded rule.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 7086e841711b263366bb385872bc1d4fb40cfa58
https://github.com/acl2/acl2/commit/7086e841711b263366bb385872bc1d4fb40cfa58
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)

Changed paths:
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/bv/arith.lisp

Log Message:
-----------
[bv] Drop unneeded rule.

Also tweak a rule.


Commit: f33a0a9f2af987a8eda420f5604265eb41625e6f
https://github.com/acl2/acl2/commit/f33a0a9f2af987a8eda420f5604265eb41625e6f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)

Changed paths:
M books/kestrel/axe/rules1.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
M books/kestrel/bv-lists/bv-array-read.lisp
M books/kestrel/x86/read-and-write.lisp

Log Message:
-----------
[bv-lists] Small improvements.


Commit: e73abde9d4f16c09c906e370c10829fa8742a0fb
https://github.com/acl2/acl2/commit/e73abde9d4f16c09c906e370c10829fa8742a0fb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)

Changed paths:
M books/GNUmakefile
M books/build/cert.pl
M books/build/doc.lisp

Log Message:
-----------
Merge.


Commit: 4302f71be44093574bd1fa24660c2c059b6e94a4
https://github.com/acl2/acl2/commit/4302f71be44093574bd1fa24660c2c059b6e94a4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)

Changed paths:
M books/kestrel/bv-lists/array-patterns.lisp

Log Message:
-----------
[bv-lists] Improve rule.


Commit: de7c60533906fe51cf71e8a95274904e620ddc7b
https://github.com/acl2/acl2/commit/de7c60533906fe51cf71e8a95274904e620ddc7b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)

Changed paths:
M books/kestrel/axe/rules1.lisp

Log Message:
-----------
[axe] Continue cleaning up file.


Commit: 0a69673439f54d5163322f85f550bcec6ca20d32
https://github.com/acl2/acl2/commit/0a69673439f54d5163322f85f550bcec6ca20d32
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)

Changed paths:
M books/kestrel/arm/memory.lisp
M books/kestrel/arrays-2d/bv-arrays-2d.lisp
M books/kestrel/axe/arm/evaluator.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/bv-array-rules.lisp
M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/evaluator-basic.lisp
M books/kestrel/axe/evaluator-support.lisp
M books/kestrel/axe/jvm/evaluator-jvm.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/packbv-axe.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/prove-with-stp2.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/risc-v/evaluator.lisp
M books/kestrel/axe/risc-v/lifter-rules.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/rules1.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/axe/unguarded-defuns2.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/x86-rules.lisp
A books/kestrel/bv-arrays/append-arrays.lisp
A books/kestrel/bv-arrays/array-of-zeros.lisp
A books/kestrel/bv-arrays/array-patterns.lisp
A books/kestrel/bv-arrays/bv-array-clear-range.lisp
A books/kestrel/bv-arrays/bv-array-clear.lisp
A books/kestrel/bv-arrays/bv-array-conversions-gen.lisp
A books/kestrel/bv-arrays/bv-array-conversions.lisp
A books/kestrel/bv-arrays/bv-array-conversions2-tests.lisp
A books/kestrel/bv-arrays/bv-array-conversions2.lisp
A books/kestrel/bv-arrays/bv-array-if.lisp
A books/kestrel/bv-arrays/bv-array-read-chunk-little.lisp
A books/kestrel/bv-arrays/bv-array-read-rules.lisp
A books/kestrel/bv-arrays/bv-array-read.lisp
A books/kestrel/bv-arrays/bv-array-write.lisp
A books/kestrel/bv-arrays/bv-arrayp.lisp
A books/kestrel/bv-arrays/bv-arrays.lisp
A books/kestrel/bv-arrays/tests-top.lisp
A books/kestrel/bv-arrays/top.lisp
R books/kestrel/bv-lists/append-arrays.lisp
R books/kestrel/bv-lists/array-of-zeros.lisp
R books/kestrel/bv-lists/array-patterns.lisp
R books/kestrel/bv-lists/bv-array-clear-range.lisp
R books/kestrel/bv-lists/bv-array-clear.lisp
R books/kestrel/bv-lists/bv-array-conversions-gen.lisp
R books/kestrel/bv-lists/bv-array-conversions.lisp
R books/kestrel/bv-lists/bv-array-conversions2-tests.lisp
R books/kestrel/bv-lists/bv-array-conversions2.lisp
R books/kestrel/bv-lists/bv-array-if.lisp
R books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
R books/kestrel/bv-lists/bv-array-read-rules.lisp
R books/kestrel/bv-lists/bv-array-read.lisp
R books/kestrel/bv-lists/bv-array-write.lisp
R books/kestrel/bv-lists/bv-arrayp.lisp
R books/kestrel/bv-lists/bv-arrays.lisp
M books/kestrel/bv-lists/tests-top.lisp
M books/kestrel/bv-lists/top.lisp
M books/kestrel/crypto/salsa/salsa20.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/java/atj/types-for-bv-fns.lisp
M books/kestrel/jvm/jvm.lisp
M books/kestrel/x86/bytes-loadedp.lisp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/support64.lisp
M books/kestrel/x86/tools/lifter-support.lisp

Log Message:
-----------
[bv-arrays] Split out bv-array material into new library.


Compare: https://github.com/acl2/acl2/compare/de69359deaa6...0a69673439f5

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/master

Commit: e7228d909d64f7964f260e59a16a23ead2ed0ca6
https://github.com/acl2/acl2/commit/e7228d909d64f7964f260e59a16a23ead2ed0ca6
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-27 (Fri, 27 Mar 2026)

Changed paths:
M books/kestrel/arm/memory.lisp
M books/kestrel/arrays-2d/bv-arrays-2d.lisp
M books/kestrel/axe/arm/evaluator.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/bv-array-rules.lisp
M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/evaluator-basic.lisp
M books/kestrel/axe/evaluator-support.lisp
M books/kestrel/axe/jvm/evaluator-jvm.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/packbv-axe.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/prove-with-stp2.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/risc-v/evaluator.lisp
M books/kestrel/axe/risc-v/lifter-rules.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp

M books/kestrel/axe/rule-lists.lisp

M books/kestrel/bv/arith.lisp

M books/kestrel/crypto/salsa/salsa20.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/java/atj/types-for-bv-fns.lisp
M books/kestrel/jvm/jvm.lisp
M books/kestrel/x86/bytes-loadedp.lisp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/support64.lisp
M books/kestrel/x86/tools/lifter-support.lisp

Log Message:
-----------

Merge commit '0a69673439f54d5163322f85f550bcec6ca20d32' into HEAD


Compare: https://github.com/acl2/acl2/compare/045c9b28cba1...e7228d909d64

[acl2buildserver]

Branch: refs/heads/testing