[acl2/acl2] fc6b35: [axe] Build in equal-of-bvsx-and-constant.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: fc6b353180667ce8e13de887e5aaf044684c2d69
https://github.com/acl2/acl2/commit/fc6b353180667ce8e13de887e5aaf044684c2d69
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

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

Log Message:
-----------
[axe] Build in equal-of-bvsx-and-constant.


Commit: 6f6bf836d9584e5c2174af1ea782ca72faf10e4c
https://github.com/acl2/acl2/commit/6f6bf836d9584e5c2174af1ea782ca72faf10e4c
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-25 (Tue, 25 Nov 2025)

Changed paths:
M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/node-replacement-array3.lisp
M books/kestrel/axe/prove-with-stp-tests.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/bv-lists/top.lisp
M books/kestrel/bv/bif.lisp
M books/kestrel/bv/bit-to-bool.lisp
M books/kestrel/bv/bitnot.lisp
M books/kestrel/bv/bitwise.lisp
M books/kestrel/bv/bitxnor.lisp
M books/kestrel/bv/bool-to-bit.lisp
M books/kestrel/bv/bvminus-rules.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvnot.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/rules12.lisp
M books/kestrel/bv/std.lisp
M books/kestrel/bv/validation-stp.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
M books/kestrel/prime-fields/bv-rules-axe.lisp

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


Commit: 2358dbaa807a25b31971d96b8f5ad1d49f07f055
https://github.com/acl2/acl2/commit/2358dbaa807a25b31971d96b8f5ad1d49f07f055
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/support.lisp

Log Message:
-----------
[axe/x86] Improve rules.


Commit: c2337970409f2467e710dca64843bd9723bc8fe6
https://github.com/acl2/acl2/commit/c2337970409f2467e710dca64843bd9723bc8fe6
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/x86-rules.lisp
A books/kestrel/x86/support64.lisp
M books/kestrel/x86/top.lisp

Log Message:
-----------
[axe/x86] Organize some rules.


Commit: afb36f36608395f8d1121e91a1744034150928cd
https://github.com/acl2/acl2/commit/afb36f36608395f8d1121e91a1744034150928cd
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

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

Log Message:
-----------
[axe/x86] Comment out rule.


Commit: 4f7504ea70b04a7bd9ed43550aa3f398a6091d2a
https://github.com/acl2/acl2/commit/4f7504ea70b04a7bd9ed43550aa3f398a6091d2a
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/integer-length.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv/bvlt.lisp

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


Compare: https://github.com/acl2/acl2/compare/22cc9f8fa90c...4f7504ea70b0

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

[acl2buildserver]

Branch: refs/heads/master

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

Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:

M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/rule-lists.lisp

M books/kestrel/axe/x86/x86-rules.lisp
A books/kestrel/x86/support64.lisp
M books/kestrel/x86/top.lisp

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

Merge commit '4f7504ea70b04a7bd9ed43550aa3f398a6091d2a' into HEAD


Compare: https://github.com/acl2/acl2/compare/291f9dee9dfe...2e73b6035784

[acl2buildserver]

Branch: refs/heads/testing