[acl2/acl2] 353caf: [bv] Add rule to replace b-not.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 353caf549b664a07480efee051f45545610c7a0d
https://github.com/acl2/acl2/commit/353caf549b664a07480efee051f45545610c7a0d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/bv/bitops.lisp

Log Message:
-----------
[bv] Add rule to replace b-not.


Commit: 814da4f2b60a8169161118377216f5cde281cc58
https://github.com/acl2/acl2/commit/814da4f2b60a8169161118377216f5cde281cc58
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/bv/bvshl.lisp
M books/kestrel/bv/single-bit.lisp

Log Message:
-----------
[bv] Add misc rules.


Commit: 7cb941c97efd69c4f4685137440a241801358e1a
https://github.com/acl2/acl2/commit/7cb941c97efd69c4f4685137440a241801358e1a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/x86/package.lsp

Log Message:
-----------
[x86] Extend package.


Commit: 74d87547d622ab48db79fd01bdbd28d8416597c9
https://github.com/acl2/acl2/commit/74d87547d622ab48db79fd01bdbd28d8416597c9
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/x86/alt-defs.lisp

Log Message:
-----------
[x86] Add rule to replace blsi.


Commit: 1ecf4c3957895f8af3c8620a217601e2baecf38d
https://github.com/acl2/acl2/commit/1ecf4c3957895f8af3c8620a217601e2baecf38d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
[axe] Clarify.


Commit: 3f890e3a03092c0d80557fe8c255b166d1820ab9
https://github.com/acl2/acl2/commit/3f890e3a03092c0d80557fe8c255b166d1820ab9
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

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

Log Message:
-----------
[axe/x86] Improve rule-lists.


Commit: cd23b3dfca518aaf613a2a9ccfdaa79641a30114
https://github.com/acl2/acl2/commit/cd23b3dfca518aaf613a2a9ccfdaa79641a30114
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/make-axe-rules.lisp

Log Message:
-----------
[axe] Drop package prefixes.


Commit: 813799d5e031eff48228e00b10dfb9aa2b233e53
https://github.com/acl2/acl2/commit/813799d5e031eff48228e00b10dfb9aa2b233e53
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/bv-lists/bv-list-read-chunk-little.lisp

Log Message:
-----------
[bv-lists] Drop package prefixes.


Commit: c70ce59293dda83bbe2d094a85b31ecafd5a8f04
https://github.com/acl2/acl2/commit/c70ce59293dda83bbe2d094a85b31ecafd5a8f04
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/bv/bvmult-rules.lisp
M books/kestrel/bv/bvplus.lisp
M books/kestrel/bv/rules12.lisp

Log Message:
-----------
[bv] Clean up a bit.


Commit: b3d63d23349cf77fded920546e8e1ca5adfd4bbc
https://github.com/acl2/acl2/commit/b3d63d23349cf77fded920546e8e1ca5adfd4bbc
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/axe-trees.lisp
M books/kestrel/axe/darg-trees.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/step-increments.lisp

Log Message:
-----------
[axe] Clean up a bit.


Commit: cc7b1c131261320dfe06dff7b3d016c2b07541a7
https://github.com/acl2/acl2/commit/cc7b1c131261320dfe06dff7b3d016c2b07541a7
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
A books/kestrel/fty/integer-list-result.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
A books/kestrel/remora/check-keywords.lisp
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/fresh-variables.lisp
M books/kestrel/remora/grammar.abnf
A books/kestrel/remora/integer-list-operations.lisp
R books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/library-extensions.lisp
M books/kestrel/remora/nat-list-operations.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/proofs/utilities/sys-view/paging/gather-paging-structures.lisp
M books/projects/x86isa/utils/paging-structures.lisp
M books/projects/x86isa/utils/records-0.lisp
M books/projects/x86isa/utils/utilities.lisp

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


Commit: e6ed2b305c5d1779b3fe51f58c4f401e2b80d9bf
https://github.com/acl2/acl2/commit/e6ed2b305c5d1779b3fe51f58c4f401e2b80d9bf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
M books/kestrel/bv/bvshl.lisp

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


Compare: https://github.com/acl2/acl2/compare/15ddbfaa3c47...e6ed2b305c5d

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

[Eric W. Smith]

Branch: refs/heads/master

[acl2buildserver]

Branch: refs/heads/testing

Commit: 853faf044022fb039c06d2c7c50e0ae046bd5720
https://github.com/acl2/acl2/commit/853faf044022fb039c06d2c7c50e0ae046bd5720
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:

M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/axe-trees.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/darg-trees.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/make-axe-rules.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/step-increments.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv-lists/bv-list-read-chunk-little.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bvmult-rules.lisp
M books/kestrel/bv/bvplus.lisp
M books/kestrel/bv/bvshl.lisp
M books/kestrel/bv/rules12.lisp
M books/kestrel/bv/single-bit.lisp
M books/kestrel/x86/alt-defs.lisp

M books/kestrel/x86/package.lsp

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

Merge commit 'e6ed2b305c5d1779b3fe51f58c4f401e2b80d9bf' into HEAD


Compare: https://github.com/acl2/acl2/compare/77b5a16e6d7f...853faf044022