[acl2/acl2] 137f51: [axe/x86] Drop unneeded rules and includes.

0 views
Skip to first unread message

Eric W. Smith

unread,
Aug 12, 2026, 4:59:17 PM (7 days ago) Aug 12
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 137f51d72d87e56e529a5fd0ff41999f376fa3bf
https://github.com/acl2/acl2/commit/137f51d72d87e56e529a5fd0ff41999f376fa3bf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_al_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ax_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_eax_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_al.lisp

Log Message:
-----------
[axe/x86] Drop unneeded rules and includes.



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

Eric W. Smith

unread,
Aug 12, 2026, 6:10:01 PM (7 days ago) Aug 12
to acl2-...@googlegroups.com
Branch: refs/heads/master

Eric W. Smith

unread,
Aug 12, 2026, 6:10:41 PM (7 days ago) Aug 12
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages