feat: add scripts for evaluation of bv performance (#718)

`compare-leansat-vs-bitwuzla` sets the width of bitvector in tested
files to different values and run the tests `reps` times.

SSA/Projects/InstCombine/HackersDelight/ch2_1DeMorgan.lean

@@ -8,43 +8,43 @@ namespace Ch2Basics
 
 namespace DeMorgansLawsExtended
 
-variable {x y z : BitVec w}
+variable {x y z : BitVec 64}
 
 theorem not_and_eq_not_or_not :
     ~~~ (x &&& y) = ~~~ x ||| ~~~ y := by
-  bv_auto
+  bv_compare'
 
 theorem not_or_eq_not_and_not :
     ~~~ (x ||| y) = ~~~ x &&& ~~~ y := by
-  bv_auto
+  bv_compare'
 
 theorem not_add_one_eq_not_sub_one :
     ~~~ (x + 1) = ~~~ x - 1 := by
-  bv_auto
+  bv_compare'
 
 theorem not_sub_one_eq_not_add_one :
     ~~~ (x - 1) = ~~~ x + 1 := by
-  bv_auto
+  bv_compare'
 
 theorem not_neg_eq_sub_one :
     ~~~ (- x) = x - 1 := by
-  bv_auto
+  bv_compare'
 
 theorem not_xor_eq_not_xor :
     ~~~ (x ^^^ y) = ~~~ x ^^^ y := by
-  bv_auto
+  bv_compare'
 
 theorem q_not_xor :
     ~~~ (x ^^^ y) = ~~~ x ^^^ y := by
-  bv_auto
+  bv_compare'
 
 theorem not_add_eq_not_sub :
     ~~~ (x + y) = ~~~ x - y := by
-  bv_auto
+  bv_compare'
 
 theorem not_sub_eq_not_add :
     ~~~ (x - y) = ~~~ x + y := by
-  bv_auto
+  bv_compare'
 
 end DeMorgansLawsExtended
 

SSA/Projects/InstCombine/HackersDelight/ch2_2AdditionAndLogicalOps.lean

@@ -10,7 +10,7 @@ namespace AdditionCombinedWithLogicalOperations
 
 set_option bv.ac_nf false
 
-variable {x y z : BitVec 32}
+variable {x y z : BitVec 64}
 
 theorem neg_eq_not_add_one :
     -x = ~~~ x + 1 := by

SSA/Projects/InstCombine/HackersDelight/ch2_3LogicalArithmeticIneq.lean

@@ -1,4 +1,3 @@
-import SSA.Projects.InstCombine.ForStd
 import SSA.Projects.InstCombine.TacticAuto
 
 set_option linter.unusedTactic false
@@ -7,7 +6,7 @@ set_option linter.unreachableTactic false
 namespace HackersDelight
 
 namespace Ch2Basics
-variable {x y z : BitVec 32}
+variable {x y z : BitVec 16}
 
 /- 2–3 Inequalities among Logical and Arithmetic Expressions -/
 

SSA/Projects/InstCombine/TacticAuto.lean

@@ -186,6 +186,6 @@ macro "bv_compare'": tactic =>
   `(tactic|
       (
         -- bv_compare "/usr/local/bin/bitwuzla"
-        bv_decide
+        bv_decide -- replace this with bv_compare to evaluate performance
       )
    )

bv-evaluation/compare-leansat-vs-bitwuzla.py

@@ -0,0 +1,33 @@
+import subprocess
+import os 
+
+results_dir = "bv-evaluation/results/"
+
+benchmark_dir = "../SSA/Projects/InstCombine/HackersDelight/"
+benchmark_dir_lake = "SSA.Projects.InstCombine.HackersDelight"
+
+reps = 1
+
+bv_width = [4, 8, 16, 32, 64]
+
+# import Leanwuzla and uncomment relevant line 
+
+subprocess.Popen('sed -i \'\' -E \'s,-- import Leanwuzla,import Leanwuzla,g\' ../SSA/Projects/InstCombine/TacticAuto.lean', shell=True).wait()
+subprocess.Popen('sed -i \'\' -E \'s,-- bv_compare \",bv_compare \",g\' ../SSA/Projects/InstCombine/TacticAuto.lean', shell=True).wait()
+subprocess.Popen('sed -i \'\' -E \'s,bv_decide -- replace this with bv_compare to evaluate performance,-- bv_decide -- replace this with bv_compare to evaluate performance,g\' ../SSA/Projects/InstCombine/TacticAuto.lean', shell=True).wait()
+
+
+for file in os.listdir(benchmark_dir):
+    print(file)
+    if "ch2_3" not in file: # currently discard broken chapter
+        for bvw in bv_width:
+            subprocess.Popen('sed -i \'\' -E \'s/variable {x y z : BitVec .+}/variable {x y z : BitVec '+str(bvw)+'}/g\' '+benchmark_dir+file, shell=True).wait()
+            # replace any sorrys with bv_compare'
+            subprocess.Popen('sed -i \'\' -E \'s,sorry,bv_compare\'\\\'\',g\' '+benchmark_dir+file, shell=True).wait()
+            for r in range(reps):
+                print(f'cd .. && lake build '+benchmark_dir_lake+'.'+file.split(".")[0]+' 2>&1 > '+results_dir+file.split(".")[0]+'_'+str(bvw)+'_'+'r'+str(r)+'.txt')
+                subprocess.Popen(f'cd .. && lake build '+benchmark_dir_lake+'.'+file.split(".")[0]+' 2>&1 > '+results_dir+file.split(".")[0]+'_'+str(bvw)+'_'+'r'+str(r)+'.txt', shell=True).wait()
+
+subprocess.Popen('sed -i \'\' -E \'s,import Leanwuzla,-- import Leanwuzla,g\' ../SSA/Projects/InstCombine/TacticAuto.lean', shell=True).wait()
+subprocess.Popen('sed -i \'\' -E \'s,bv_compare \",-- bv_compare \",g\' ../SSA/Projects/InstCombine/TacticAuto.lean', shell=True).wait()
+subprocess.Popen('sed -i \'\' -E \'s,-- bv_decide -- replace this with bv_compare to evaluate performance,bv_decide -- replace this with bv_compare to evaluate performance,g\' ../SSA/Projects/InstCombine/TacticAuto.lean', shell=True).wait()