chore: unify bv_auto and bv_bench (#858)

opencompl · Nov 15, 2024 · def2cfa · def2cfa
1 parent 05e5442
commit def2cfa
Show file tree

Hide file tree

Showing 5 changed files with 106 additions and 9 deletions.
diff --git a/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean
@@ -45,6 +45,7 @@ theorem alive_DivRemOfSelect (w : Nat) :
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
+  simp_alive_split
   alive_auto
 
 end AliveHandwritten
diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -44,6 +44,7 @@ theorem alive_DivRemOfSelect (w : Nat) :
   simp_alive_ssa
   simp_alive_undef
   simp_alive_case_bash
+  simp_alive_split
   alive_auto
 
 /--info: 'AliveHandwritten.DivRemOfSelect.alive_DivRemOfSelect' depends on
@@ -413,7 +414,9 @@ def alive_simplifyAndOrXor2515 (w : Nat) :
   simp only [simp_llvm_wrap]
   simp_alive_ssa
   simp_alive_undef
+  simp_alive_ops
   simp_alive_case_bash
+  simp_alive_split
   alive_auto
 
 /-- info: 'AliveHandwritten.AndOrXor.alive_simplifyAndOrXor2515' depends on axioms: